From e12110637730d067c216abcc86185b761189b342 Mon Sep 17 00:00:00 2001
From: vblot <24938579+vblot@users.noreply.github.com>
Date: Fri, 28 May 2021 18:29:37 +0200
Subject: getting rid of native-coq (#95)

---
 src/_CoqProject | 153 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 153 insertions(+)
 create mode 100644 src/_CoqProject

(limited to 'src/_CoqProject')

diff --git a/src/_CoqProject b/src/_CoqProject
new file mode 100644
index 0000000..f7862e1
--- /dev/null
+++ b/src/_CoqProject
@@ -0,0 +1,153 @@
+########################################################################
+##   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 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
-- 
cgit