V8.9 (#43)

* New syntax for implicit arguments

* Towards 8.9: problems with Micromega plugin

* Move to _CoqProject

* Back to name Makefile

* Switch to Makefile.local instead of -extra

* The compilation issue is a Coq bug

* Ok with 8.9

* INSTALL with 8.9

* Everything ok with 8.9

1 files changed, 0 insertions, 169 deletions

diff --git a/src/versions/standard/Make b/src/versions/standard/Make
deleted file mode 100644
index e275b8f..0000000
--- a/src/versions/standard/Make
+++ /dev/null
@@ -1,169 +0,0 @@
-########################################################################
-##   This file is intended to developers: please do not use it        ##
-## directly, rather use the "configure.sh" script.                    ##
-########################################################################
-
-
-
-
-########################################################################
-## To generate the Makefile:                                          ##
-##   coq_makefile -f Make -o Makefile                                 ##
-## In the Makefile :                                                  ##
-## 1) Add "-native" to the CAMLDEP command (ocamldep -native ...)     ##
-## 2) remove "post-all" from the targets "all" and "all.timing.diff"  ##
-########################################################################
-
-
--R . SMTCoq
-
--I .
--I bva
--I classes
--I array
--I cnf
--I euf
--I lfsc
--I lia
--I smtlib2
--I trace
--I verit
--I zchaff
--I versions/standard
--I versions/standard/Int63
--I versions/standard/Array
-
-# -I "$(shell $(COQBIN)coqc -where)/plugins/micromega"
-
--extra "test" "" "cd ../unit-tests; make"
--extra "ztest" "" "cd ../unit-tests; make zchaff"
--extra "vtest" "" "cd ../unit-tests; make verit"
--extra "lfsctest" "" "cd ../unit-tests; make lfsc"
-
--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 smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml" ""
-
-CAMLLEX = $(CAMLBIN)ocamllex
-CAMLYACC = $(CAMLBIN)ocamlyacc
-
-versions/standard/Int63/Int63.v
-versions/standard/Int63/Int63Native.v
-versions/standard/Int63/Int63Op.v
-versions/standard/Int63/Int63Axioms.v
-versions/standard/Int63/Int63Properties.v
-versions/standard/Array/PArray.v
-
-versions/standard/Structures.v
-versions/standard/structures.ml
-versions/standard/structures.mli
-
-bva/BVList.v
-bva/Bva_checker.v
-
-classes/SMT_classes.v
-classes/SMT_classes_instances.v
-
-array/FArray.v
-array/Array_checker.v
-
-trace/coqTerms.ml
-trace/coqTerms.mli
-trace/smtBtype.ml
-trace/smtBtype.mli
-trace/satAtom.ml
-trace/satAtom.mli
-trace/smtAtom.ml
-trace/smtAtom.mli
-trace/smtCertif.ml
-trace/smtCertif.mli
-trace/smtCnf.ml
-trace/smtCnf.mli
-trace/smtCommands.ml
-trace/smtCommands.mli
-trace/smtForm.ml
-trace/smtForm.mli
-trace/smtMisc.ml
-trace/smtMisc.mli
-trace/smtTrace.ml
-trace/smtTrace.mli
-
-smtlib2/smtlib2_parse.ml
-smtlib2/smtlib2_parse.mli
-smtlib2/smtlib2_lex.ml
-smtlib2/smtlib2_lex.mli
-smtlib2/smtlib2_ast.ml
-smtlib2/smtlib2_ast.mli
-smtlib2/smtlib2_genConstr.ml
-smtlib2/smtlib2_genConstr.mli
-smtlib2/smtlib2_util.ml
-smtlib2/smtlib2_util.mli
-smtlib2/sExpr.ml
-smtlib2/sExpr.mli
-smtlib2/smtlib2_solver.ml
-smtlib2/smtlib2_solver.mli
-smtlib2/sExprParser.ml
-smtlib2/sExprParser.mli
-smtlib2/sExprLexer.ml
-
-verit/veritParser.ml
-verit/veritParser.mli
-verit/veritLexer.ml
-verit/veritLexer.mli
-verit/verit.ml
-verit/verit.mli
-verit/veritSyntax.ml
-verit/veritSyntax.mli
-
-lfsc/shashcons.mli
-lfsc/shashcons.ml
-lfsc/hstring.mli
-lfsc/hstring.ml
-lfsc/lfscParser.ml
-lfsc/lfscParser.mli
-lfsc/type.ml
-lfsc/ast.ml
-lfsc/ast.mli
-lfsc/translator_sig.mli
-lfsc/builtin.ml
-lfsc/tosmtcoq.ml
-lfsc/tosmtcoq.mli
-lfsc/converter.ml
-lfsc/lfsc.ml
-lfsc/lfscLexer.ml
-
-zchaff/cnfParser.ml
-zchaff/cnfParser.mli
-zchaff/satParser.ml
-zchaff/satParser.mli
-zchaff/zchaff.ml
-zchaff/zchaff.mli
-zchaff/zchaffParser.ml
-zchaff/zchaffParser.mli
-
-cnf/Cnf.v
-
-euf/Euf.v
-
-lia/lia.ml
-lia/lia.mli
-lia/Lia.v
-
-spl/Assumptions.v
-spl/Syntactic.v
-spl/Arithmetic.v
-spl/Operators.v
-
-Conversion_tactics.v
-Misc.v
-SMTCoq.v
-ReflectFacts.v
-PropToBool.v
-BoolToProp.v
-Tactics.v
-SMT_terms.v
-State.v
-Trace.v
-
-g_smtcoq.ml4
-smtcoq_plugin.mlpack