diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-05-28 19:15:25 +0200 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-05-28 19:15:25 +0200 |
commit | be486d634803e7bdfd455e58dbe3ed0968798eda (patch) | |
tree | 8bba73ba41522a4fb288dc7243bd3954932b7366 /src/_CoqProject | |
parent | a3a63ab0bceb12f03bac91ef7461061f1cb20af1 (diff) | |
parent | b40fefbb52afbc7deaa0b591d155bf2e84d0afba (diff) | |
download | smtcoq-be486d634803e7bdfd455e58dbe3ed0968798eda.tar.gz smtcoq-be486d634803e7bdfd455e58dbe3ed0968798eda.zip |
Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11
Diffstat (limited to 'src/_CoqProject')
-rw-r--r-- | src/_CoqProject | 155 |
1 files changed, 155 insertions, 0 deletions
diff --git a/src/_CoqProject b/src/_CoqProject new file mode 100644 index 0000000..ebecac9 --- /dev/null +++ b/src/_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 ## +## sed -i 's/^CAMLDONTLINK=unix,str$/CAMLDONTLINK=num,str,unix,dynlink,threads/' Makefile ## +## WARNING: DO NOT FORGET THE SECOND LINE (see PR#62) ## +######################################################################## + + +-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 Int63 +-I Array +-I ../3rdparty/alt-ergo + +Int63/Int63.v +Int63/Int63Native.v +Int63/Int63Op.v +Int63/Int63Axioms.v +Int63/Int63Properties.v +Array/PArray.v + +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 +trace/coqInterface.ml +trace/coqInterface.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.mlg +smtcoq_plugin.mlpack |