diff options
Diffstat (limited to 'src/versions/standard/_CoqProject')
-rw-r--r-- | src/versions/standard/_CoqProject | 159 |
1 files changed, 0 insertions, 159 deletions
diff --git a/src/versions/standard/_CoqProject b/src/versions/standard/_CoqProject deleted file mode 100644 index 86dd443..0000000 --- a/src/versions/standard/_CoqProject +++ /dev/null @@ -1,159 +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 ## -######################################################################## - - --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 ../3rdparty/alt-ergo - -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/smtMaps.ml -trace/smtMaps.mli -trace/smtMisc.ml -trace/smtMisc.mli -trace/smtTrace.ml -trace/smtTrace.mli - -../3rdparty/alt-ergo/smtlib2_parse.ml -../3rdparty/alt-ergo/smtlib2_parse.mli -../3rdparty/alt-ergo/smtlib2_lex.ml -../3rdparty/alt-ergo/smtlib2_lex.mli -../3rdparty/alt-ergo/smtlib2_ast.ml -../3rdparty/alt-ergo/smtlib2_ast.mli -../3rdparty/alt-ergo/smtlib2_util.ml -../3rdparty/alt-ergo/smtlib2_util.mli - -smtlib2/smtlib2_genConstr.ml -smtlib2/smtlib2_genConstr.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 -QInst.v -Tactics.v -SMT_terms.v -State.v -Trace.v - -g_smtcoq.ml4 -smtcoq_plugin.mlpack |