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