aboutsummaryrefslogtreecommitdiffstats
path: root/src/versions/native
diff options
context:
space:
mode:
authorQuentin Garchery <garchery.quentin@gmail.com>2018-10-28 00:30:23 +0200
committerValentin Blot <24938579+vblot@users.noreply.github.com>2018-10-28 00:30:23 +0200
commit7940ef63c654be26b41ce20162207f3c67d0b10a (patch)
tree89d7e2a04b93a0cb37642416535637ddb45eba8b /src/versions/native
parentcefda895d15a3f7eb7bf75402beb6fae22162585 (diff)
downloadsmtcoq-7940ef63c654be26b41ce20162207f3c67d0b10a.tar.gz
smtcoq-7940ef63c654be26b41ce20162207f3c67d0b10a.zip
New files SmtBtype.ml(i) for module formerly in SmtAtom
Diffstat (limited to 'src/versions/native')
-rw-r--r--src/versions/native/Make4
-rw-r--r--src/versions/native/Makefile4
2 files changed, 6 insertions, 2 deletions
diff --git a/src/versions/native/Make b/src/versions/native/Make
index c6ce237..69cbbfb 100644
--- a/src/versions/native/Make
+++ b/src/versions/native/Make
@@ -40,7 +40,7 @@
-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/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 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) -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 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 = smtcoq.cmxa
@@ -59,6 +59,8 @@ 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
diff --git a/src/versions/native/Makefile b/src/versions/native/Makefile
index d443fe9..61c8c01 100644
--- a/src/versions/native/Makefile
+++ b/src/versions/native/Makefile
@@ -185,6 +185,7 @@ MLFILES:=lia/lia.ml\
trace/smtCommands.ml\
trace/smtCnf.ml\
trace/smtCertif.ml\
+ trace/smtBtype.ml\
trace/smtAtom.ml\
trace/satAtom.ml\
trace/coqTerms.ml\
@@ -213,6 +214,7 @@ MLIFILES:=lia/lia.mli\
trace/smtCommands.mli\
trace/smtCnf.mli\
trace/smtCertif.mli\
+ trace/smtBtype.mli\
trace/smtAtom.mli\
trace/satAtom.mli\
trace/coqTerms.mli\
@@ -285,7 +287,7 @@ beautify: $(VFILES:=.beautified)
$(CMXS): $(CMXA)
$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^
-$(CMXA): 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 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): 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 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
$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^
ml: verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml