aboutsummaryrefslogtreecommitdiffstats
path: root/src/versions/standard/Make
diff options
context:
space:
mode:
Diffstat (limited to 'src/versions/standard/Make')
-rw-r--r--src/versions/standard/Make11
1 files changed, 6 insertions, 5 deletions
diff --git a/src/versions/standard/Make b/src/versions/standard/Make
index 42d0552..c833f4d 100644
--- a/src/versions/standard/Make
+++ b/src/versions/standard/Make
@@ -15,7 +15,7 @@
## 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 ##
+## - 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 ##
########################################################################
@@ -40,11 +40,11 @@
-custom "$(CAMLYACC) $<" "%.mly" "%.ml %.mli"
-custom "" "verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml" "ml"
--custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "versions/standard/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 smtlib2/smtlib2_util.cmx smtlib2/smtlib2_ast.cmx smtlib2/smtlib2_parse.cmx smtlib2/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx trace/smt_tactic.cmx" "$(CMXA)"
+-custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "versions/standard/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 smtlib2/smtlib2_util.cmx smtlib2/smtlib2_ast.cmx smtlib2/smtlib2_parse.cmx smtlib2/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx smtcoq_plugin.cmx" "$(CMXA)"
-custom "$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^" "$(CMXA)" "$(CMXS)"
-CMXA = trace/smtcoq.cmxa
-CMXS = trace/smt_tactic.cmxs
+CMXA = smtcoq.cmxa
+CMXS = smtcoq_plugin.cmxs
CAMLLEX = $(CAMLBIN)ocamllex
CAMLYACC = $(CAMLBIN)ocamlyacc
@@ -70,7 +70,6 @@ trace/smtCommands.ml
trace/smtForm.ml
trace/smtForm.mli
trace/smtMisc.ml
-trace/smt_tactic.ml4
trace/smtTrace.ml
smtlib2/smtlib2_parse.ml
@@ -109,3 +108,5 @@ SMTCoq.v
SMT_terms.v
State.v
Trace.v
+
+smtcoq_plugin.ml4