########################################################################
##   This file is intended to developers, please do not use it to     ##
## generate a Makefile, rather use the provided Makefile.             ##
########################################################################




########################################################################
## To generate the Makefile:                                          ##
##   coq_makefile -f Make -o Makefile                                 ##
## Suppress the "Makefile" target                                     ##

## Change the "all" target into:                                      ##
##   all: ml $(CMXFILES) $(CMXA) $(CMXS) $(VOFILES)                   ##
## Change the "install-natdynlink" target: change CMXSFILES into CMXS and add the same thing for CMXA. ##
## Change the "install" target: change CMO into CMX.                  ##
## Remove the automatically generated line with %.cmxs: %.cmx         ##
## Finally, suppress the "Makefile" target and add to the "clean" target: ##
##   - rm -f ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.mli smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtcoq.a ##
########################################################################


-R . SMTCoq

-I .
-I cnf
-I euf
-I lia
-I smtlib2
-I trace
-I verit
-I zchaff
-I versions/standard
-I versions/standard/Int63
-I versions/standard/Array

-I $(COQBIN)../plugins/micromega

# -extra "test" "" "cd ../unit-tests; make" ""
# -extra "ztest" "" "cd ../unit-tests; make zchaff"
# -extra "vtest" "" "cd ../unit-tests; make verit"

-extra "%.ml" "%.mll" "$(CAMLLEX) $<"
-extra "%.ml %.mli" "%.mly" "$(CAMLYACC) $<"
-extra-phony "smtcoq_plugin.mlpack.d" "verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml" ""

CAMLLEX = $(CAMLBIN)ocamllex
CAMLYACC = $(CAMLBIN)ocamlyacc

versions/standard/Int63/Int63.v
versions/standard/Int63/Int63Native.v
versions/standard/Int63/Int63Op.v
versions/standard/Int63/Int63Axioms.v
versions/standard/Int63/Int63Properties.v
versions/standard/Array/PArray.v

versions/standard/Structures.v
versions/standard/structures.ml

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

smtlib2/smtlib2_parse.ml
smtlib2/smtlib2_parse.mli
smtlib2/smtlib2_ast.ml
smtlib2/smtlib2_genConstr.ml
smtlib2/smtlib2_lex.ml
smtlib2/smtlib2_util.ml

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

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

cnf/Cnf.v

euf/Euf.v

lia/lia.ml
lia/Lia.v

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

Misc.v
SMTCoq.v
SMT_terms.v
State.v
Trace.v

g_smtcoq.ml4
smtcoq_plugin.mlpack