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, 155 insertions, 0 deletions

diff --git a/src/versions/standard/_CoqProject b/src/versions/standard/_CoqProject
new file mode 100644
index 0000000..a71f500
--- /dev/null
+++ b/src/versions/standard/_CoqProject
@@ -0,0 +1,155 @@
+########################################################################
+##   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                                 ##
+########################################################################
+
+
+-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
+
+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/mutils_full.ml
+versions/standard/mutils_full.mli
+versions/standard/coq_micromega_full.ml
+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