diff options
Diffstat (limited to 'src/versions/standard/Makefile')
| -rw-r--r-- | src/versions/standard/Makefile | 67 |
1 files changed, 61 insertions, 6 deletions
diff --git a/src/versions/standard/Makefile b/src/versions/standard/Makefile index 0225e3c..f71b0c8 100644 --- a/src/versions/standard/Makefile +++ b/src/versions/standard/Makefile @@ -2,7 +2,7 @@ ## v # The Coq Proof Assistant ## ## <O___,, # INRIA - CNRS - LIX - LRI - PPS ## ## \VV/ # ## -## // # Makefile automagically generated by coq_makefile V8.6 ## +## // # Makefile automagically generated by coq_makefile V8.6.1 ## ############################################################################# # WARNING @@ -55,8 +55,12 @@ vo_to_obj = $(addsuffix .o,\ ########################## OCAMLLIBS?=-I "."\ + -I "bva"\ + -I "classes"\ + -I "array"\ -I "cnf"\ -I "euf"\ + -I "lfsc"\ -I "lia"\ -I "smtlib2"\ -I "trace"\ @@ -69,8 +73,12 @@ OCAMLLIBS?=-I "."\ COQLIBS?=\ -R "." SMTCoq\ -I "."\ + -I "bva"\ + -I "classes"\ + -I "array"\ -I "cnf"\ -I "euf"\ + -I "lfsc"\ -I "lia"\ -I "smtlib2"\ -I "trace"\ @@ -132,6 +140,7 @@ COQSRCLIBS?=-I "$(COQLIB)kernel" \ -I "$(COQLIB)/plugins/firstorder" \ -I "$(COQLIB)/plugins/fourier" \ -I "$(COQLIB)/plugins/funind" \ + -I "$(COQLIB)/plugins/ltac" \ -I "$(COQLIB)/plugins/micromega" \ -I "$(COQLIB)/plugins/nsatz" \ -I "$(COQLIB)/plugins/omega" \ @@ -188,6 +197,12 @@ VFILES:=versions/standard/Int63/Int63.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\ @@ -198,6 +213,10 @@ VFILES:=versions/standard/Int63/Int63.v\ Conversion_tactics.v\ Misc.v\ SMTCoq.v\ + ReflectFacts.v\ + PropToBool.v\ + BoolToProp.v\ + Tactics.v\ SMT_terms.v\ State.v\ Trace.v @@ -249,10 +268,24 @@ MLFILES:=versions/standard/structures.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\ @@ -297,10 +330,19 @@ MLIFILES:=versions/standard/structures.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\ @@ -397,13 +439,16 @@ ztest: vtest: cd ../unit-tests; make verit +lfsctest: + cd ../unit-tests; make lfsc + %.ml: %.mll $(CAMLLEX) $< %.ml %.mli: %.mly $(CAMLYACC) $< -smtcoq_plugin.mlpack.d: verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml +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 ################### # # @@ -504,12 +549,20 @@ uninstall: uninstall_me.sh @echo "B $(COQLIB)config" >> .merlin @echo "B $(COQLIB)ltac" >> .merlin @echo "B $(COQLIB)engine" >> .merlin - @echo "B /home/valentin/smtcoq/smtcoq/src/versions/standard" >> .merlin - @echo "S /home/valentin/smtcoq/smtcoq/src/versions/standard" >> .merlin + @echo "B /home/artemis/Recherche/github.com/ckeller/smtcoq-lfsc/src/versions/standard" >> .merlin + @echo "S /home/artemis/Recherche/github.com/ckeller/smtcoq-lfsc/src/versions/standard" >> .merlin + @echo "B bva" >> .merlin + @echo "S bva" >> .merlin + @echo "B classes" >> .merlin + @echo "S classes" >> .merlin + @echo "B array" >> .merlin + @echo "S array" >> .merlin @echo "B cnf" >> .merlin @echo "S cnf" >> .merlin @echo "B euf" >> .merlin @echo "S euf" >> .merlin + @echo "B lfsc" >> .merlin + @echo "S lfsc" >> .merlin @echo "B lia" >> .merlin @echo "S lia" >> .merlin @echo "B smtlib2" >> .merlin @@ -541,10 +594,11 @@ clean:: - rm -rf test - rm -rf ztest - rm -rf vtest - - rm -f ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.mli smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml + - rm -rf lfsctest + - rm -f ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.mli smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtlib2/sExprParser.mli smtlib2/sExprParser.ml smtlib2/sExprLexer.ml cleanall:: clean - rm -f $(patsubst %.v,.%.aux,$(VFILES)) + rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux) archclean:: rm -f *.cmx *.o @@ -558,6 +612,7 @@ printenv: @echo 'COQLIBINSTALL = $(COQLIBINSTALL)' @echo 'COQDOCINSTALL = $(COQDOCINSTALL)' + ################### # # # Implicit rules. # |