diff options
| author | Quentin Garchery <garchery.quentin@gmail.com> | 2018-10-28 00:30:23 +0200 |
|---|---|---|
| committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2018-10-28 00:30:23 +0200 |
| commit | 7940ef63c654be26b41ce20162207f3c67d0b10a (patch) | |
| tree | 89d7e2a04b93a0cb37642416535637ddb45eba8b /src/versions | |
| parent | cefda895d15a3f7eb7bf75402beb6fae22162585 (diff) | |
| download | smtcoq-7940ef63c654be26b41ce20162207f3c67d0b10a.tar.gz smtcoq-7940ef63c654be26b41ce20162207f3c67d0b10a.zip | |
New files SmtBtype.ml(i) for module formerly in SmtAtom
Diffstat (limited to 'src/versions')
| -rw-r--r-- | src/versions/native/Make | 4 | ||||
| -rw-r--r-- | src/versions/native/Makefile | 4 | ||||
| -rw-r--r-- | src/versions/standard/Make | 2 | ||||
| -rw-r--r-- | src/versions/standard/Makefile | 2 | ||||
| -rw-r--r-- | src/versions/standard/smtcoq_plugin_standard.mlpack | 1 |
5 files changed, 11 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 diff --git a/src/versions/standard/Make b/src/versions/standard/Make index 37822db..b674ce9 100644 --- a/src/versions/standard/Make +++ b/src/versions/standard/Make @@ -60,6 +60,8 @@ versions/standard/structures.mli trace/coqTerms.ml trace/coqTerms.mli +trace/smtBtype.ml +trace/smtBtype.mli trace/satAtom.ml trace/satAtom.mli trace/smtAtom.ml diff --git a/src/versions/standard/Makefile b/src/versions/standard/Makefile index 9d2a5de..0225e3c 100644 --- a/src/versions/standard/Makefile +++ b/src/versions/standard/Makefile @@ -235,6 +235,7 @@ endif MLFILES:=versions/standard/structures.ml\ trace/coqTerms.ml\ + trace/smtBtype.ml\ trace/satAtom.ml\ trace/smtAtom.ml\ trace/smtCertif.ml\ @@ -282,6 +283,7 @@ endif MLIFILES:=versions/standard/structures.mli\ trace/coqTerms.mli\ + trace/smtBtype.mli\ trace/satAtom.mli\ trace/smtAtom.mli\ trace/smtCertif.mli\ diff --git a/src/versions/standard/smtcoq_plugin_standard.mlpack b/src/versions/standard/smtcoq_plugin_standard.mlpack index 3ab358b..b316040 100644 --- a/src/versions/standard/smtcoq_plugin_standard.mlpack +++ b/src/versions/standard/smtcoq_plugin_standard.mlpack @@ -2,6 +2,7 @@ Structures SmtMisc CoqTerms +SmtBtype SmtForm SmtCertif SmtTrace |