diff options
Diffstat (limited to 'src/versions/standard/Makefile.conf')
-rw-r--r-- | src/versions/standard/Makefile.conf | 103 |
1 files changed, 0 insertions, 103 deletions
diff --git a/src/versions/standard/Makefile.conf b/src/versions/standard/Makefile.conf deleted file mode 100644 index 928db7d..0000000 --- a/src/versions/standard/Makefile.conf +++ /dev/null @@ -1,103 +0,0 @@ -# This configuration file was generated by running: -# coq_makefile -f Make -o Makefile - - -############################################################################### -# # -# Project files. # -# # -############################################################################### - -COQMF_VFILES = 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 bva/BVList.v bva/Bva_checker.v classes/SMT_classes.v classes/SMT_classes_instances.v array/FArray.v array/Array_checker.v cnf/Cnf.v euf/Euf.v 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 -COQMF_MLIFILES = versions/standard/structures.mli trace/coqTerms.mli trace/smtBtype.mli trace/satAtom.mli trace/smtAtom.mli trace/smtCertif.mli trace/smtCnf.mli trace/smtCommands.mli trace/smtForm.mli trace/smtMisc.mli trace/smtTrace.mli smtlib2/smtlib2_parse.mli smtlib2/smtlib2_lex.mli smtlib2/smtlib2_ast.mli smtlib2/smtlib2_genConstr.mli smtlib2/smtlib2_util.mli smtlib2/sExpr.mli smtlib2/smtlib2_solver.mli smtlib2/sExprParser.mli verit/veritParser.mli verit/veritLexer.mli verit/verit.mli verit/veritSyntax.mli lfsc/shashcons.mli lfsc/hstring.mli lfsc/lfscParser.mli lfsc/ast.mli lfsc/translator_sig.mli lfsc/tosmtcoq.mli zchaff/cnfParser.mli zchaff/satParser.mli zchaff/zchaff.mli zchaff/zchaffParser.mli lia/lia.mli -COQMF_MLFILES = versions/standard/structures.ml trace/coqTerms.ml trace/smtBtype.ml trace/satAtom.ml trace/smtAtom.ml trace/smtCertif.ml trace/smtCnf.ml trace/smtCommands.ml trace/smtForm.ml trace/smtMisc.ml trace/smtTrace.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtlib2/smtlib2_ast.ml smtlib2/smtlib2_genConstr.ml smtlib2/smtlib2_util.ml smtlib2/sExpr.ml smtlib2/smtlib2_solver.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml verit/veritParser.ml verit/veritLexer.ml verit/verit.ml verit/veritSyntax.ml lfsc/shashcons.ml lfsc/hstring.ml lfsc/lfscParser.ml lfsc/type.ml lfsc/ast.ml lfsc/builtin.ml lfsc/tosmtcoq.ml lfsc/converter.ml lfsc/lfsc.ml lfsc/lfscLexer.ml zchaff/cnfParser.ml zchaff/satParser.ml zchaff/zchaff.ml zchaff/zchaffParser.ml lia/lia.ml -COQMF_ML4FILES = g_smtcoq.ml4 -COQMF_MLPACKFILES = smtcoq_plugin.mlpack -COQMF_MLLIBFILES = - -############################################################################### -# # -# Path directives (-I, -R, -Q). # -# # -############################################################################### - -COQMF_OCAMLLIBS = -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' -COQMF_SRC_SUBDIRS = . bva classes array cnf euf lfsc lia smtlib2 trace verit zchaff versions/standard versions/standard/Int63 versions/standard/Array '$(shell $(COQBIN)coqc -where)/plugins/micromega' -COQMF_COQLIBS = -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' -R . SMTCoq -COQMF_COQLIBS_NOML = -R . SMTCoq - -############################################################################### -# # -# Coq configuration. # -# # -############################################################################### - -COQMF_LOCAL=1 -COQMF_COQLIB=/home/artemis/Autres/coq-8.7.2// -COQMF_DOCDIR=/home/artemis/Autres/coq-8.7.2/doc/ -COQMF_OCAMLFIND=/usr/bin/ocamlfind -COQMF_CAMLP4=camlp5 -COQMF_CAMLP4O=/usr/bin/camlp5o -COQMF_CAMLP4BIN=/usr/bin/ -COQMF_CAMLP4LIB=/usr/lib/ocaml/camlp5 -COQMF_CAMLP4OPTIONS=-loc loc -COQMF_CAMLFLAGS=-thread -rectypes -w +a-4-9-27-41-42-44-45-48-50 -safe-string -COQMF_HASNATDYNLINK=true -COQMF_COQ_SRC_SUBDIRS=config dev lib kernel library engine pretyping interp parsing proofs tactics toplevel printing intf grammar ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/fourier plugins/funind plugins/ltac plugins/micromega plugins/nsatz plugins/omega plugins/quote plugins/romega plugins/rtauto plugins/setoid_ring plugins/ssr plugins/ssrmatching plugins/syntax plugins/xml -COQMF_WINDRIVE=/home/artemis/Autres/coq-8.7.2 - -############################################################################### -# # -# Extra variables. # -# # -############################################################################### - -CAMLLEX = $(CAMLBIN)ocamllex -CAMLYACC = $(CAMLBIN)ocamlyacc -COQMF_OTHERFLAGS = -COQMF_INSTALLCOQDOCROOT = SMTCoq - -############################################################################### -# # -# Extra targets. (-extra and -extra-phony, DEPRECATED) # -# # -############################################################################### - -post-all:: - $(MAKE) -f $(SELF) test -clean:: - rm -f test -test : - cd ../unit-tests; make - -post-all:: - $(MAKE) -f $(SELF) ztest -clean:: - rm -f ztest -ztest : - cd ../unit-tests; make zchaff - -post-all:: - $(MAKE) -f $(SELF) vtest -clean:: - rm -f vtest -vtest : - cd ../unit-tests; make verit - -post-all:: - $(MAKE) -f $(SELF) lfsctest -clean:: - rm -f lfsctest -lfsctest : - cd ../unit-tests; make lfsc - -%.ml : %.mll - $(CAMLLEX) $< - -%.ml %.mli : %.mly - $(CAMLYACC) $< - -.PHONY: smtcoq_plugin.mlpack.d -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 - - |