diff options
| author | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2018-10-25 16:41:06 +0200 |
|---|---|---|
| committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2018-10-25 16:41:06 +0200 |
| commit | 9c2efdde9c4b68e5314c4fb1c0dedcea0d138bb5 (patch) | |
| tree | 947c33f64fbaf25a4a230b29bbe33c7c4ad0e8cb /src/versions/standard | |
| parent | 2e21fade829b79ced140080b68b9efe07a83e922 (diff) | |
| download | smtcoq-9c2efdde9c4b68e5314c4fb1c0dedcea0d138bb5.tar.gz smtcoq-9c2efdde9c4b68e5314c4fb1c0dedcea0d138bb5.zip | |
conversion tactics
Diffstat (limited to 'src/versions/standard')
| -rw-r--r-- | src/versions/standard/Make | 1 | ||||
| -rw-r--r-- | src/versions/standard/Makefile | 11 |
2 files changed, 6 insertions, 6 deletions
diff --git a/src/versions/standard/Make b/src/versions/standard/Make index 8defd9b..5322133 100644 --- a/src/versions/standard/Make +++ b/src/versions/standard/Make @@ -117,6 +117,7 @@ spl/Syntactic.v spl/Arithmetic.v spl/Operators.v +Conversion_tactics.v Misc.v SMTCoq.v SMT_terms.v diff --git a/src/versions/standard/Makefile b/src/versions/standard/Makefile index 84c10d9..9d2a5de 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.1 ## +## // # Makefile automagically generated by coq_makefile V8.6 ## ############################################################################# # WARNING @@ -132,7 +132,6 @@ 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" \ @@ -196,6 +195,7 @@ VFILES:=versions/standard/Int63/Int63.v\ spl/Syntactic.v\ spl/Arithmetic.v\ spl/Operators.v\ + Conversion_tactics.v\ Misc.v\ SMTCoq.v\ SMT_terms.v\ @@ -502,8 +502,8 @@ uninstall: uninstall_me.sh @echo "B $(COQLIB)config" >> .merlin @echo "B $(COQLIB)ltac" >> .merlin @echo "B $(COQLIB)engine" >> .merlin - @echo "B /home/artemis/Recherche/Github/smtcoq/smtcoq/src/versions/standard" >> .merlin - @echo "S /home/artemis/Recherche/Github/smtcoq/smtcoq/src/versions/standard" >> .merlin + @echo "B /home/valentin/smtcoq/smtcoq/src/versions/standard" >> .merlin + @echo "S /home/valentin/smtcoq/smtcoq/src/versions/standard" >> .merlin @echo "B cnf" >> .merlin @echo "S cnf" >> .merlin @echo "B euf" >> .merlin @@ -542,7 +542,7 @@ clean:: - 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 cleanall:: clean - rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux) + rm -f $(patsubst %.v,.%.aux,$(VFILES)) archclean:: rm -f *.cmx *.o @@ -556,7 +556,6 @@ printenv: @echo 'COQLIBINSTALL = $(COQLIBINSTALL)' @echo 'COQDOCINSTALL = $(COQDOCINSTALL)' - ################### # # # Implicit rules. # |