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

2 files changed, 55 insertions, 5 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index 652542825..33b95c2f5 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -713,7 +713,33 @@ let prterm = pr_lconstr
 (* Printer function for sets of Assumptions.assumptions.
    It is used primarily by the Print Assumptions command. *)
 
-open Assumptions
+type context_object =
+  | Variable of Id.t (* A section variable or a Let definition *)
+  | Axiom of constant * (Label.t * Context.rel_context * types) list
+  | Opaque of constant     (* An opaque constant. *)
+  | Transparent of constant
+
+(* Defines a set of [assumption] *)
+module OrderedContextObject =
+struct
+  type t = context_object
+  let compare x y =
+      match x , y with
+      | Variable i1 , Variable i2 -> Id.compare i1 i2
+      | Axiom (k1,_) , Axiom (k2, _) -> con_ord k1 k2
+      | Opaque k1 , Opaque k2 -> con_ord k1 k2
+      | Transparent k1 , Transparent k2 -> con_ord k1 k2
+      | Axiom _ , Variable _ -> 1
+      | Opaque _ , Variable _
+      | Opaque _ , Axiom _ -> 1
+      | Transparent _ , Variable _
+      | Transparent _ , Axiom _
+      | Transparent _ , Opaque _ -> 1
+      | _ , _ -> -1
+end
+
+module ContextObjectSet = Set.Make (OrderedContextObject)
+module ContextObjectMap = Map.Make (OrderedContextObject)
 
 let pr_assumptionset env s =
   if ContextObjectMap.is_empty s then
@@ -729,15 +755,29 @@ let pr_assumptionset env s =
       try str " : " ++ pr_ltype typ
       with e when Errors.noncritical e -> mt ()
     in
+    let safe_pr_ltype_relctx (rctx, typ) =
+      let sigma, env = get_current_context () in
+      let env = Environ.push_rel_context rctx env in
+      try str " " ++ pr_ltype_env env sigma typ
+      with e when Errors.noncritical e -> mt ()
+    in
     let fold t typ accu =
       let (v, a, o, tr) = accu in
       match t with
       | Variable id ->
         let var = str (Id.to_string id) ++ str " : " ++ pr_ltype typ in
         (var :: v, a, o, tr)
-      | Axiom kn ->
+      | Axiom (kn,[]) ->
         let ax = safe_pr_constant env kn ++ safe_pr_ltype typ in
         (v, ax :: a, o, tr)
+      | Axiom (kn,l) ->
+        let ax = safe_pr_constant env kn ++ safe_pr_ltype typ ++
+          cut() ++
+          prlist_with_sep cut (fun (lbl, ctx, ty) ->
+            str " used in " ++ str (Names.Label.to_string lbl) ++
+            str " to prove:" ++ safe_pr_ltype_relctx (ctx,ty))
+          l in
+        (v, ax :: a, o, tr)
       | Opaque kn ->
         let opq = safe_pr_constant env kn ++ safe_pr_ltype typ in
         (v, a, opq :: o, tr)
diff --git a/printing/printer.mli b/printing/printer.mli
index a469a8dbe..5f56adbe6 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