diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-03-02 13:16:12 +0100 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-03-02 13:16:12 +0100 |
commit | e3ff85dccf62b497cd017d2b55e08e7f49ebd80f (patch) | |
tree | 8386e6f8989a8770062eb796ee4fd0be3fab082f /src/versions/native/Make | |
parent | 5705e360d5948369639939c08ef9f77328fb8226 (diff) | |
download | smtcoq-e3ff85dccf62b497cd017d2b55e08e7f49ebd80f.tar.gz smtcoq-e3ff85dccf62b497cd017d2b55e08e7f49ebd80f.zip |
Removed old port to Coq 8.4
Diffstat (limited to 'src/versions/native/Make')
-rw-r--r-- | src/versions/native/Make | 93 |
1 files changed, 0 insertions, 93 deletions
diff --git a/src/versions/native/Make b/src/versions/native/Make deleted file mode 100644 index 5d173e0..0000000 --- a/src/versions/native/Make +++ /dev/null @@ -1,93 +0,0 @@ -######################################################################## -## 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/*.vo ../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 --I versions/native - --custom "cd ../unit-tests; make" "" "test" --custom "cd ../unit-tests; make zchaff" "" "ztest" --custom "cd ../unit-tests; make verit" "" "vtest" - --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 $@ $^" "versions/native/structures.cmx 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 - -versions/native/structures.ml - -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 |