From 33f7877dc675cd1c2ce5ffd8da04e65b4d029676 Mon Sep 17 00:00:00 2001
From: SimonBoulier
Date: Mon, 5 Nov 2018 11:45:47 +0100
Subject: Add [Print Typing Flags] command.

---
 printing/printer.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index ec1b9b8e49..9c74d8cfbb 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -1003,3 +1003,8 @@ let print_and_diff oldp newp =
         pr_open_subgoals ~proof
     in
     Feedback.msg_notice output;;
+
+let pr_typing_flags flags =
+  str "check_guarded: " ++ bool flags.check_guarded ++ fnl ()
+  ++ str "check_positive: " ++ bool flags.check_positive ++ fnl ()
+  ++ str "check_universes: " ++ bool flags.check_universes
-- 
cgit v1.2.3


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 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'printing/printer.ml')

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
-- 
cgit v1.2.3


From 3ae2b2383dc20a8c128acc4a090a41a5a236034b Mon Sep 17 00:00:00 2001
From: SimonBoulier
Date: Thu, 6 Jun 2019 11:06:03 +0200
Subject: Fix Print Assumptions: Inductive types can have unsafe fixpoints or 
 type-in-type universes

---
 printing/printer.ml | 28 +++++++++++++++++-----------
 1 file changed, 17 insertions(+), 11 deletions(-)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index b8f25eb380..e3225fadd5 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -853,8 +853,8 @@ let pr_goal_emacs ~proof gid sid =
 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 *)
+  | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *)
+  | TypeInType of GlobRef.t (* a constant which relies on type in type *)
 
 type context_object =
   | Variable of Id.t (* A section variable or a Let definition *)
@@ -874,7 +874,7 @@ struct
     | Positive m1 , Positive m2 ->
         MutInd.CanOrd.compare m1 m2
     | Guarded k1 , Guarded k2 ->
-        Constant.CanOrd.compare k1 k2
+        GlobRef.Ordered.compare k1 k2
     | _ , Constant _ -> 1
     | _ , Positive _ -> 1
     | _ -> -1
@@ -904,14 +904,20 @@ let pr_assumptionset env sigma s =
     let safe_pr_constant env kn =
       try pr_constant env kn
       with Not_found ->
-        (* FIXME? *)
-        let mp,lab = Constant.repr2 kn in
-        str (ModPath.to_string mp) ++ str "." ++ Label.print lab
+        Names.Constant.print kn
+    in
+    let safe_pr_global env gr =
+      try pr_global_env (Termops.vars_of_env env) gr
+      with Not_found ->
+        let open GlobRef in match gr with
+        | VarRef id -> Id.print id
+        | ConstRef con -> Constant.print con
+        | IndRef (mind,_) -> MutInd.print mind
+        | ConstructRef _ -> assert false
     in
     let safe_pr_inductive env kn =
       try pr_inductive env (kn,0)
       with Not_found ->
-        (* FIXME? *)
         MutInd.print kn
     in
     let safe_pr_ltype env sigma typ =
@@ -929,10 +935,10 @@ let pr_assumptionset env sigma s =
           safe_pr_constant env kn ++ safe_pr_ltype env sigma typ
       | Positive m ->
           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 assumed to be guarded.")
-      | TypeInType kn ->
-         hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"relies on an unsafe hierarchy.")
+      | Guarded gr ->
+          hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"is assumed to be guarded.")
+      | TypeInType gr ->
+         hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"relies on an unsafe hierarchy.")
     in
     let fold t typ accu =
       let (v, a, o, tr) = accu in
-- 
cgit v1.2.3