From 671e556453c1eee335cf788ebc72675f5a7483d8 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 29 Jun 2015 21:34:11 +0200
Subject: win: compile with -debug

---
 dev/make-installer-win32.sh | 2 +-
 dev/make-installer-win64.sh | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'dev')

diff --git a/dev/make-installer-win32.sh b/dev/make-installer-win32.sh
index ec7cd5773a..c6ed2f401d 100755
--- a/dev/make-installer-win32.sh
+++ b/dev/make-installer-win32.sh
@@ -5,7 +5,7 @@ ZIP=_make.zip
 URL1=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-bin.zip/download
 URL2=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-dep.zip/download
 
-[ -e config/Makefile ] || ./configure -prefix ./ -with-doc no
+[ -e config/Makefile ] || ./configure -debug -prefix ./ -with-doc no
 make -j2 
 if [ ! -e bin/make.exe ]; then
   wget -O $ZIP $URL1 && 7z x $ZIP "bin/*"
diff --git a/dev/make-installer-win64.sh b/dev/make-installer-win64.sh
index 73e1fdbeb2..03fdda4aa1 100755
--- a/dev/make-installer-win64.sh
+++ b/dev/make-installer-win64.sh
@@ -5,13 +5,13 @@ ZIP=_make.zip
 URL1=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-bin.zip/download
 URL2=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-dep.zip/download
 
-[ -e config/Makefile ] || ./configure -prefix ./ -with-doc no
+[ -e config/Makefile ] || ./configure -debug -prefix ./ -with-doc no
 make -j2 coqide
 mkdir -p bin32
 cp bin/* bin32/
 make clean
 make archclean
-( . ${BASE}_64/environ; ./configure -prefix ./ -with-doc no; make -j2; make ide/coqidetop.cmxs )
+( . ${BASE}_64/environ; ./configure -debug -prefix ./ -with-doc no; make -j2; make ide/coqidetop.cmxs )
 cp bin32/coqide* bin/
 if [ ! -e bin/make.exe ]; then
   wget -O $ZIP $URL1 && 7z x $ZIP "bin/*"
-- 
cgit v1.2.3


From 2defd4c15467736b73f69adb501e3a4fe2111ce5 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 29 Jun 2015 21:30:19 +0200
Subject: Assumptions: more informative print for False axiom (Close: #4054)

When an axiom of an empty type is matched in order to inhabit
a type, do print that type (as if each use of that axiom was a
distinct foo_subproof).

E.g.

  Lemma w : True.
  Proof. case demon. Qed.

  Lemma x y : y = 0 /\ True /\ forall w, w = y.
  Proof. split. case demon. split; [ exact w | case demon ]. Qed.

  Print Assumptions x.

Prints:

  Axioms:
  demon : False
   used in x to prove: forall w : nat, w = y
   used in w to prove: True
   used in x to prove: y = 0
---
 dev/printers.mllib | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 74f36f6f5a..07b48ed573 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -110,7 +110,6 @@ Loadpath
 Goptions
 Decls
 Heads
-Assumptions
 Keys
 Locusops
 Miscops
@@ -204,6 +203,7 @@ Hints
 Himsg
 Cerrors
 Locality
+Assumptions
 Vernacinterp
 Dischargedhypsmap
 Discharge
-- 
cgit v1.2.3