From ae455fa3aa29c872c9c5b2736fff861afebcd051 Mon Sep 17 00:00:00 2001 From: ckeller Date: Fri, 15 Mar 2019 11:23:55 +0100 Subject: 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 --- src/versions/standard/Make | 169 --------------------------------------------- 1 file changed, 169 deletions(-) delete mode 100644 src/versions/standard/Make (limited to 'src/versions/standard/Make') 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 -- cgit