Fix Print Assumptions: Inductive types can have unsafe fixpoints or

 type-in-type universes

4 files changed, 47 insertions, 22 deletions

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
diff --git a/printing/printer.mli b/printing/printer.mli
index f397b2b643..788f303aee 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -191,8 +191,8 @@ val print_and_diff : Proof.t option -> Proof.t option -> unit
 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 *)
diff --git a/test-suite/success/typing_flags.v b/test-suite/success/typing_flags.v
index c15701e000..bd20d9c804 100644
--- a/test-suite/success/typing_flags.v
+++ b/test-suite/success/typing_flags.v
@@ -36,3 +36,8 @@ Inductive Cor :=
 
 Set Positivity Checking.
 Print Assumptions Cor.
+
+Inductive Box :=
+| box : forall n, f n = n -> g 2 -> Box.
+
+Print Assumptions Box.
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index e9c347c9bb..a72e43de01 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -313,13 +313,13 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
         if cb.const_typing_flags.check_guarded then accu
         else
           let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
-          ContextObjectMap.add (Axiom (Guarded kn, l)) Constr.mkProp accu
+          ContextObjectMap.add (Axiom (Guarded obj, l)) Constr.mkProp accu
       in
       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
+          ContextObjectMap.add (Axiom (TypeInType obj, l)) Constr.mkProp accu
       in
     if not (Declareops.constant_has_body cb) then
       let t = type_of_constant cb in
@@ -335,10 +335,24 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
       accu
   | IndRef (m,_) | ConstructRef ((m,_),_) ->
       let mind = lookup_mind m in
-      if mind.mind_typing_flags.check_positive then
-        accu
-      else
-        let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
-        ContextObjectMap.add (Axiom (Positive m, l)) Constr.mkProp accu
-  in
-  GlobRef.Map_env.fold fold graph ContextObjectMap.empty
+      let accu =
+        if mind.mind_typing_flags.check_positive then accu
+        else
+          let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
+          ContextObjectMap.add (Axiom (Positive m, l)) Constr.mkProp accu
+      in
+      let accu =
+        if mind.mind_typing_flags.check_guarded then accu
+        else
+          let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
+          ContextObjectMap.add (Axiom (Guarded obj, l)) Constr.mkProp accu
+      in
+      let accu =
+        if mind.mind_typing_flags.check_universes then accu
+        else
+          let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
+          ContextObjectMap.add (Axiom (TypeInType obj, l)) Constr.mkProp accu
+      in
+      accu
+
+  in GlobRef.Map_env.fold fold graph ContextObjectMap.empty