########################################################################
##   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                                 ##
## 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 and VCMXS. ##
## Change the "install" target: change CMO into CMX.                  ##
## Finally, suppress the "Makefile" target and add to the "clean" target: ##
##   - rm -f NSMTCoq* cnf/NSMTCoq* euf/NSMTCoq* lia/NSMTCoq* spl/NSMTCoq* ../unit-tests/NSMTCoq* ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml verit/smtlib2_parse.mli verit/smtlib2_parse.ml verit/smtlib2_lex.ml ##
########################################################################


-R . SMTCoq

-I cnf
-I euf
-I lia
-I trace
-I verit
-I zchaff

# -custom "cd ../unit-tests; make" "" "logs"
-custom "cd ../unit-tests; make" "" "test"

-custom "$(CAMLLEX) $<" "%.mll" "%.ml"
-custom "$(CAMLYACC) $<" "%.mly" "%.ml %.mli"
-custom "" "verit/veritParser.ml verit/veritLexer.ml verit/smtlib2_parse.ml verit/smtlib2_lex.ml" "ml"

-custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "trace/smtMisc.cmx trace/coqTerms.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx verit/smtlib2_util.cmx verit/smtlib2_ast.cmx verit/smtlib2_parse.cmx verit/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx verit/smtlib2_genConstr.cmx verit/verit.cmx trace/smt_tactic.cmx" "$(CMXA)"
-custom "$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^" "$(CMXA)" "$(CMXS)"

CMXA = trace/smtcoq.cmxa
CMXS = trace/smt_tactic.cmxs
VCMXS = "NSMTCoq_State.cmxs NSMTCoq_Misc.cmxs NSMTCoq_SMT_terms.cmxs cnf/NSMTCoq_cnf_Cnf.cmxs euf/NSMTCoq_euf_Euf.cmxs lia/NSMTCoq_lia_Lia.cmxs spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Arithmetic.cmxs spl/NSMTCoq_spl_Operators.cmxs NSMTCoq_Trace.cmxs NSMTCoq_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.cmi NSMTCoq_SMT_terms.cmi cnf/NSMTCoq_cnf_Cnf.cmi euf/NSMTCoq_euf_Euf.cmi lia/NSMTCoq_lia_Lia.cmi spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Arithmetic.cmi spl/NSMTCoq_spl_Operators.cmi NSMTCoq_Trace.cmi NSMTCoq_Trace.cmi NSMTCoq_SMTCoq.cmi"
CAMLLEX = $(CAMLBIN)ocamllex
CAMLYACC = $(CAMLBIN)ocamlyacc

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

verit/smtlib2_ast.ml
verit/smtlib2_genConstr.ml
verit/smtlib2_lex.ml
verit/smtlib2_parse.ml
verit/smtlib2_util.ml
verit/veritParser.ml
verit/veritLexer.ml
verit/verit.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/Syntactic.v
spl/Arithmetic.v
spl/Operators.v

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

# tests/Tests.v