From 889603e7a2ed41b890e43729aa0abf90bebd3ca6 Mon Sep 17 00:00:00 2001
From: SimonBoulier
Date: Mon, 3 Jun 2019 16:04:54 +0200
Subject: Improve [Print Assumptions] for type-in-type and assumed positive.

---
 printing/printer.ml   | 7 +++++--
 printing/printer.mli  | 1 +
 vernac/assumptions.ml | 8 +++++++-
 3 files changed, 13 insertions(+), 3 deletions(-)

diff --git a/printing/printer.ml b/printing/printer.ml
index 9c74d8cfbb..b8f25eb380 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -854,6 +854,7 @@ type axiom =
   | Constant of Constant.t (* An axiom or a constant. *)
   | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
   | Guarded of Constant.t (* a constant whose (co)fixpoints have been assumed to be guarded *)
+  | TypeInType of Constant.t (* a constant which relies on type in type *)
 
 type context_object =
   | Variable of Id.t (* A section variable or a Let definition *)
@@ -927,9 +928,11 @@ let pr_assumptionset env sigma s =
       | Constant kn ->
           safe_pr_constant env kn ++ safe_pr_ltype env sigma typ
       | Positive m ->
-          hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is positive.")
+          hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is assumed to be positive.")
       | Guarded kn ->
-          hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"is positive.")
+          hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"is assumed to be guarded.")
+      | TypeInType kn ->
+         hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"relies on an unsafe hierarchy.")
     in
     let fold t typ accu =
       let (v, a, o, tr) = accu in
diff --git a/printing/printer.mli b/printing/printer.mli
index 0855f2d109..f397b2b643 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -192,6 +192,7 @@ type axiom =
   | Constant of Constant.t (* An axiom or a constant. *)
   | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
   | Guarded of Constant.t (* a constant whose (co)fixpoints have been assumed to be guarded *)
+  | TypeInType of Constant.t (* a constant which relies on type in type *)
 
 type context_object =
   | Variable of Id.t (* A section variable or a Let definition *)
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index cbdc84e073..e9c347c9bb 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -315,7 +315,13 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
           let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
           ContextObjectMap.add (Axiom (Guarded kn, l)) Constr.mkProp accu
       in
-    if not (Declareops.constant_has_body cb) || not cb.const_typing_flags.check_universes then
+      let accu =
+        if cb.const_typing_flags.check_universes then accu
+        else
+          let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
+          ContextObjectMap.add (Axiom (TypeInType kn, l)) Constr.mkProp accu
+      in
+    if not (Declareops.constant_has_body cb) then
       let t = type_of_constant cb in
       let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
       ContextObjectMap.add (Axiom (Constant kn,l)) t accu
-- 
cgit v1.2.3