From 98bf2facf5a61758897d000c4a7d1d6c6c2965fb Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Sat, 30 Apr 2016 03:03:50 +0200
Subject: 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

---
 src/versions/standard/Makefile | 63 +++++++++++++++++++++++++++++++++++++-----
 1 file changed, 56 insertions(+), 7 deletions(-)

(limited to 'src/versions/standard/Makefile')

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)
-- 
cgit