diff options
Diffstat (limited to 'src/versions/standard/Make')
| -rw-r--r-- | src/versions/standard/Make | 23 |
1 files changed, 12 insertions, 11 deletions
diff --git a/src/versions/standard/Make b/src/versions/standard/Make index 3834ee0..7c4497e 100644 --- a/src/versions/standard/Make +++ b/src/versions/standard/Make @@ -9,6 +9,8 @@ ######################################################################## ## To generate the Makefile: ## ## coq_makefile -f Make -o Makefile ## +## Suppress the "Makefile" target ## + ## 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. ## @@ -21,6 +23,7 @@ -R . SMTCoq +-I . -I cnf -I euf -I lia @@ -32,19 +35,16 @@ -I versions/standard/Int63 -I versions/standard/Array --custom "cd ../unit-tests; make" "" "test" --custom "cd ../unit-tests; make zchaff" "" "ztest" --custom "cd ../unit-tests; make verit" "" "vtest" +-I $(COQBIN)../plugins/micromega --custom "$(CAMLLEX) $<" "%.mll" "%.ml" --custom "$(CAMLYACC) $<" "%.mly" "%.ml %.mli" --custom "" "verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml" "ml" +# -extra "test" "" "cd ../unit-tests; make" "" +# -extra "ztest" "" "cd ../unit-tests; make zchaff" +# -extra "vtest" "" "cd ../unit-tests; make verit" --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)" +-extra "%.ml" "%.mll" "$(CAMLLEX) $<" +-extra "%.ml %.mli" "%.mly" "$(CAMLYACC) $<" +-extra-phony "smtcoq_plugin.mlpack.d" "verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml" "" -CMXA = smtcoq.cmxa -CMXS = smtcoq_plugin.cmxs CAMLLEX = $(CAMLBIN)ocamllex CAMLYACC = $(CAMLBIN)ocamlyacc @@ -107,4 +107,5 @@ SMT_terms.v State.v Trace.v -smtcoq_plugin.ml4 +g_smtcoq.ml4 +smtcoq_plugin.mlpack |