########################################################################
##   This file is intended to developers: please do not use it        ##
## directly, rather use the "configure.sh" script.                    ##
########################################################################




########################################################################
## To generate the Makefile:                                          ##
##   coq_makefile -f Make -o Makefile                                 ##
##   sed -i 's/^CAMLDONTLINK=unix,str$/CAMLDONTLINK=num,str,unix,dynlink,threads/' Makefile ##
## WARNING: DO NOT FORGET THE SECOND LINE (see PR#62)                 ##
########################################################################


-R . SMTCoq

-I .
-I bva
-I classes
-I array
-I cnf
-I euf
-I lfsc
-I lia
-I smtlib2
-I trace
-I verit
-I zchaff
-I PArray
-I ../3rdparty/alt-ergo

PArray/PArray.v

bva/BVList.v
bva/Bva_checker.v

classes/SMT_classes.v
classes/SMT_classes_instances.v

array/FArray.v
array/Array_checker.v

trace/coqTerms.ml
trace/coqTerms.mli
trace/smtBtype.ml
trace/smtBtype.mli
trace/satAtom.ml
trace/satAtom.mli
trace/smtAtom.ml
trace/smtAtom.mli
trace/smtCertif.ml
trace/smtCertif.mli
trace/smtCnf.ml
trace/smtCnf.mli
trace/smtCommands.ml
trace/smtCommands.mli
trace/smtForm.ml
trace/smtForm.mli
trace/smtMaps.ml
trace/smtMaps.mli
trace/smtMisc.ml
trace/smtMisc.mli
trace/smtTrace.ml
trace/smtTrace.mli
trace/coqInterface.ml
trace/coqInterface.mli

../3rdparty/alt-ergo/smtlib2_parse.ml
../3rdparty/alt-ergo/smtlib2_parse.mli
../3rdparty/alt-ergo/smtlib2_lex.ml
../3rdparty/alt-ergo/smtlib2_lex.mli
../3rdparty/alt-ergo/smtlib2_ast.ml
../3rdparty/alt-ergo/smtlib2_ast.mli
../3rdparty/alt-ergo/smtlib2_util.ml
../3rdparty/alt-ergo/smtlib2_util.mli

smtlib2/smtlib2_genConstr.ml
smtlib2/smtlib2_genConstr.mli
smtlib2/sExpr.ml
smtlib2/sExpr.mli
smtlib2/smtlib2_solver.ml
smtlib2/smtlib2_solver.mli
smtlib2/sExprParser.ml
smtlib2/sExprParser.mli
smtlib2/sExprLexer.ml

verit/veritParser.ml
verit/veritParser.mli
verit/veritLexer.ml
verit/veritLexer.mli
verit/verit.ml
verit/verit.mli
verit/veritSyntax.ml
verit/veritSyntax.mli

lfsc/shashcons.mli
lfsc/shashcons.ml
lfsc/hstring.mli
lfsc/hstring.ml
lfsc/lfscParser.ml
lfsc/lfscParser.mli
lfsc/type.ml
lfsc/ast.ml
lfsc/ast.mli
lfsc/translator_sig.mli
lfsc/builtin.ml
lfsc/tosmtcoq.ml
lfsc/tosmtcoq.mli
lfsc/converter.ml
lfsc/lfsc.ml
lfsc/lfscLexer.ml

zchaff/cnfParser.ml
zchaff/cnfParser.mli
zchaff/satParser.ml
zchaff/satParser.mli
zchaff/zchaff.ml
zchaff/zchaff.mli
zchaff/zchaffParser.ml
zchaff/zchaffParser.mli

cnf/Cnf.v

euf/Euf.v

lia/lia.ml
lia/lia.mli
lia/Lia.v

spl/Assumptions.v
spl/Syntactic.v
spl/Arithmetic.v
spl/Operators.v

Conversion_tactics.v
Misc.v
SMTCoq.v
ReflectFacts.v
PropToBool.v
QInst.v
Tactics.v
SMT_terms.v
State.v
Trace.v

g_smtcoq.mlg
smtcoq_plugin.mlpack