aboutsummaryrefslogtreecommitdiffstats
path: root/src/versions/native/Make
diff options
context:
space:
mode:
authorChantal Keller <Chantal.Keller@lri.fr>2016-03-02 13:16:12 +0100
committerChantal Keller <Chantal.Keller@lri.fr>2016-03-02 13:16:12 +0100
commite3ff85dccf62b497cd017d2b55e08e7f49ebd80f (patch)
tree8386e6f8989a8770062eb796ee4fd0be3fab082f /src/versions/native/Make
parent5705e360d5948369639939c08ef9f77328fb8226 (diff)
downloadsmtcoq-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/Make93
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