From 2defd4c15467736b73f69adb501e3a4fe2111ce5 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
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
---
 library/library.mllib | 1 -
 1 file changed, 1 deletion(-)

(limited to 'library/library.mllib')

diff --git a/library/library.mllib b/library/library.mllib
index eca28c822..920657365 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -16,5 +16,4 @@ Dischargedhypsmap
 Goptions
 Decls
 Heads
-Assumptions
 Keys
-- 
cgit v1.2.3