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
---
 printing/printer.mli | 16 +++++++++++++---
 1 file changed, 13 insertions(+), 3 deletions(-)

(limited to 'printing/printer.mli')

diff --git a/printing/printer.mli b/printing/printer.mli
index a469a8dbed..5f56adbe6f 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -160,10 +160,20 @@ val emacs_str              : string -> string
 val prterm                 : constr -> std_ppcmds (** = pr_lconstr *)
 
 
-(** spiwack: printer function for sets of Environ.assumption.
-            It is used primarily by the Print Assumption command. *)
+(** Declarations for the "Print Assumption" command *)
+type context_object =
+  | Variable of Id.t  (** A section variable or a Let definition *)
+  (** An axiom and the type it inhabits (if an axiom of the empty type) *)
+  | Axiom of constant * (Label.t * Context.rel_context * types) list
+  | Opaque of constant      (** An opaque constant. *)
+  | Transparent of constant (** A transparent constant *)
+
+module ContextObjectSet : Set.S with type elt = context_object
+module ContextObjectMap : CMap.ExtS
+  with type key = context_object and module Set := ContextObjectSet
+
 val pr_assumptionset :
-  env -> Term.types Assumptions.ContextObjectMap.t ->std_ppcmds
+  env -> Term.types ContextObjectMap.t -> std_ppcmds
 
 val pr_goal_by_id : string -> std_ppcmds
 
-- 
cgit v1.2.3