######################################################################## ## 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 ## ## In the Makefile : ## ## 1) Suppress the "Makefile" target ## ## 2) Change the "all" target into: ## ## all: ml $(CMXFILES) $(CMXA) $(CMXS) $(VOFILES) ## ## 3) Change the "install-natdynlink" target: ## ## change CMXSFILES into CMXS and add the same block for CMXA and VCMXS. ## ## 4) Change the "install" target: change CMOFILES into CMXFILES. ## ## 5) Add to the "clean" target: ## ## - rm -f NSMTCoq* cnf/NSMTCoq* euf/NSMTCoq* lia/NSMTCoq* spl/NSMTCoq* ../unit-tests/NSMTCoq* ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml ../3rdparty/alt-ergo/smtlib2_parse.mli ../3rdparty/alt-ergo/smtlib2_parse.ml ../3rdparty/alt-ergo/smtlib2_lex.ml smtlib2/sExprParser.mli smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscLexer.ml lfsc/lfscParser.ml lfsc/lfscParser.mli trace/smtcoq.a ## ######################################################################## -R . SMTCoq -I bva -I classes -I array -I cnf -I euf -I lfsc -I lia -I smtlib2 -I trace -I verit -I zchaff -I versions/native -I ../3rdparty/alt-ergo -custom "cd ../unit-tests; make vernac" "" "test" -custom "cd ../unit-tests; make zchaffv" "" "ztest" -custom "cd ../unit-tests; make veritv" "" "vtest" -custom "$(CAMLLEX) $<" "%.mll" "%.ml" -custom "$(CAMLYACC) $<" "%.mly" "%.ml %.mli" -custom "" "verit/veritParser.ml verit/veritLexer.ml ../3rdparty/alt-ergo/smtlib2_parse.ml ../3rdparty/alt-ergo/smtlib2_lex.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml" "ml" -custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "versions/native/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtBtype.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx trace/smtMaps.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx ../3rdparty/alt-ergo/smtlib2_util.cmx ../3rdparty/alt-ergo/smtlib2_ast.cmx ../3rdparty/alt-ergo/smtlib2_parse.cmx ../3rdparty/alt-ergo/smtlib2_lex.cmx smtlib2/sExpr.cmx smtlib2/sExprParser.cmx smtlib2/sExprLexer.cmx smtlib2/smtlib2_solver.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx lfsc/shashcons.cmx lfsc/hstring.cmx lfsc/type.cmx lfsc/ast.cmx lfsc/builtin.cmx lfsc/tosmtcoq.cmx lfsc/converter.cmx lfsc/lfscParser.cmx lfsc/lfscLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx lfsc/lfsc.cmx smtcoq_plugin.cmx" "$(CMXA)" -custom "$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^" "$(CMXA)" "$(CMXS)" CMXA = smtcoq.cmxa CMXS = smtcoq_plugin.cmxs VCMXS = "versions/native/NSMTCoq_versions_native_Structures.cmxs NSMTCoq_State.cmxs NSMTCoq_Misc.cmxs classes/NSMTCoq_SMT_classes.cmxs classes/NSMTCoq_SMT_classes_instances.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_Assumptions.cmxs spl/NSMTCoq_spl_Arithmetic.cmxs spl/NSMTCoq_spl_Operators.cmxs NSMTCoq_Trace.cmxs NSMTCoq_Tactics.cmxs NSMTCoq_Conversion_tactics.cmxs NSMTCoq_PropToBool.cmxs NSMTCoq_BoolToProp.cmxs NSMTCoq_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.cmi classes/NSMTCoq_SMT_classes.cmi classes/NSMTCoq_SMT_classes_instances.cmi NSMTCoq_SMT_terms.cmi cnf/NSMTCoq_cnf_Cnf.cmi euf/NSMTCoq_euf_Euf.cmi lia/NSMTCoq_lia_Lia.cmi spl/NSMTCoq_spl_Syntactic.cmi spl/NSMTCoq_spl_Assumptions.cmi spl/NSMTCoq_spl_Arithmetic.cmi spl/NSMTCoq_spl_Operators.cmi NSMTCoq_Trace.cmi NSMTCoq_Trace.cmi NSMTCoq_Tactics.cmi NSMTCoq_Conversion_tactics.cmi NSMTCoq_PropToBool.cmi NSMTCoq_BoolToProp.cmi NSMTCoq_SMTCoq.cmi" CAMLLEX = $(CAMLBIN)ocamllex CAMLYACC = $(CAMLBIN)ocamlyacc bva/BVList.v bva/Bva_checker.v classes/SMT_classes.v classes/SMT_classes_instances.v array/FArray.v array/Array_checker.v versions/native/Structures.v versions/native/structures.ml versions/native/structures.mli trace/coqTerms.ml trace/coqTerms.mli trace/satAtom.ml trace/satAtom.mli trace/smtAtom.ml trace/smtAtom.mli trace/smtBtype.ml trace/smtBtype.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 ../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/sExprParser.ml smtlib2/sExprParser.mli smtlib2/sExprLexer.ml smtlib2/sExpr.ml smtlib2/sExpr.mli smtlib2/smtlib2_solver.ml smtlib2/smtlib2_solver.mli 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/lfscLexer.ml 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 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 BoolToProp.v Tactics.v SMT_terms.v State.v Trace.v smtcoq_plugin.ml4