diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-30 03:03:50 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-30 03:03:50 +0200 |
| commit | 98bf2facf5a61758897d000c4a7d1d6c6c2965fb (patch) | |
| tree | fcb99694bdc0df548398a718676847acdc5436c3 /src/versions/standard/Makefile | |
| parent | 640bf0dda4a4880aeb525d1460dc91f5041aa626 (diff) | |
| download | smtcoq-98bf2facf5a61758897d000c4a7d1d6c6c2965fb.tar.gz smtcoq-98bf2facf5a61758897d000c4a7d1d6c6c2965fb.zip | |
Holes in proof:
- can now take learned clauses as argument
- returns a whole clause (and not only a literal)
- tested for the vernacular commands
Warning: seems to slow down 8.5 version
Diffstat (limited to 'src/versions/standard/Makefile')
| -rw-r--r-- | src/versions/standard/Makefile | 63 |
1 files changed, 56 insertions, 7 deletions
diff --git a/src/versions/standard/Makefile b/src/versions/standard/Makefile index 33ce492..cb92e59 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.5 ## +## // # Makefile automagically generated by coq_makefile V8.5pl1 ## ############################################################################# # WARNING @@ -96,12 +96,22 @@ COQDOC?="$(COQBIN)coqdoc" COQCHK?="$(COQBIN)coqchk" COQMKTOP?="$(COQBIN)coqmktop" -COQSRCLIBS?=-I "$(COQLIB)kernel" -I "$(COQLIB)lib" \ - -I "$(COQLIB)library" -I "$(COQLIB)parsing" -I "$(COQLIB)pretyping" \ - -I "$(COQLIB)interp" -I "$(COQLIB)printing" -I "$(COQLIB)intf" \ - -I "$(COQLIB)proofs" -I "$(COQLIB)tactics" -I "$(COQLIB)tools" \ - -I "$(COQLIB)toplevel" -I "$(COQLIB)stm" -I "$(COQLIB)grammar" \ - -I "$(COQLIB)config" \ +COQSRCLIBS?=-I "$(COQLIB)kernel" \ +-I "$(COQLIB)lib" \ +-I "$(COQLIB)library" \ +-I "$(COQLIB)parsing" \ +-I "$(COQLIB)pretyping" \ +-I "$(COQLIB)interp" \ +-I "$(COQLIB)printing" \ +-I "$(COQLIB)intf" \ +-I "$(COQLIB)proofs" \ +-I "$(COQLIB)tactics" \ +-I "$(COQLIB)tools" \ +-I "$(COQLIB)toplevel" \ +-I "$(COQLIB)stm" \ +-I "$(COQLIB)grammar" \ +-I "$(COQLIB)config" \ + \ -I "$(COQLIB)/plugins/btauto" \ -I "$(COQLIB)/plugins/cc" \ -I "$(COQLIB)/plugins/decl_mode" \ @@ -168,6 +178,7 @@ VFILES:=versions/standard/Int63/Int63.v\ cnf/Cnf.v\ euf/Euf.v\ lia/Lia.v\ + spl/Assumptions.v\ spl/Syntactic.v\ spl/Arithmetic.v\ spl/Operators.v\ @@ -413,6 +424,44 @@ uninstall_me.sh: Makefile uninstall: uninstall_me.sh sh $< +.merlin: + @echo 'FLG -rectypes' > .merlin + @echo "B $(COQLIB) kernel" >> .merlin + @echo "B $(COQLIB) lib" >> .merlin + @echo "B $(COQLIB) library" >> .merlin + @echo "B $(COQLIB) parsing" >> .merlin + @echo "B $(COQLIB) pretyping" >> .merlin + @echo "B $(COQLIB) interp" >> .merlin + @echo "B $(COQLIB) printing" >> .merlin + @echo "B $(COQLIB) intf" >> .merlin + @echo "B $(COQLIB) proofs" >> .merlin + @echo "B $(COQLIB) tactics" >> .merlin + @echo "B $(COQLIB) tools" >> .merlin + @echo "B $(COQLIB) toplevel" >> .merlin + @echo "B $(COQLIB) stm" >> .merlin + @echo "B $(COQLIB) grammar" >> .merlin + @echo "B $(COQLIB) config" >> .merlin + @echo "B cnf" >> .merlin + @echo "S cnf" >> .merlin + @echo "B euf" >> .merlin + @echo "S euf" >> .merlin + @echo "B lia" >> .merlin + @echo "S lia" >> .merlin + @echo "B smtlib2" >> .merlin + @echo "S smtlib2" >> .merlin + @echo "B trace" >> .merlin + @echo "S trace" >> .merlin + @echo "B verit" >> .merlin + @echo "S verit" >> .merlin + @echo "B zchaff" >> .merlin + @echo "S zchaff" >> .merlin + @echo "B versions/standard" >> .merlin + @echo "S versions/standard" >> .merlin + @echo "B versions/standard/Int63" >> .merlin + @echo "S versions/standard/Int63" >> .merlin + @echo "B versions/standard/Array" >> .merlin + @echo "S versions/standard/Array" >> .merlin + clean:: rm -f $(ALLCMOFILES) $(CMIFILES) $(CMAFILES) rm -f $(ALLCMOFILES:.cmo=.cmx) $(CMXAFILES) $(CMXSFILES) $(ALLCMOFILES:.cmo=.o) $(CMXAFILES:.cmxa=.a) |