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

1 files changed, 13 insertions, 3 deletions

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