From bc4560fa6c88aadcb2ee8312a950a7ce17fc33ee Mon Sep 17 00:00:00 2001
From: SimonBoulier
Date: Mon, 5 Nov 2018 11:18:08 +0100
Subject: Split the [check_guarded] typing_flag into [check_guarded] (for
 (co)fixpoints) and [check_positive] (for (co)inductive types).

---
 checker/values.ml      | 2 +-
 kernel/declarations.ml | 4 ++++
 kernel/declareops.ml   | 1 +
 kernel/indtypes.ml     | 2 +-
 tactics/declare.ml     | 2 +-
 vernac/assumptions.ml  | 2 +-
 vernac/indschemes.ml   | 2 +-
 7 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/checker/values.ml b/checker/values.ml
index 8dc09aed87..ac9bc26344 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -219,7 +219,7 @@ let v_cst_def =
     [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]; [|v_primitive|]|]
 
 let v_typing_flags =
-  v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|]
+  v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|]
 
 let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
 
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index dff19dee5e..8d32684b09 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -66,6 +66,10 @@ type typing_flags = {
   (** If [false] then fixed points and co-fixed points are assumed to
       be total. *)
 
+  check_positive : bool;
+  (** If [false] then inductive types are assumed positive and co-inductive
+      types are assumed productive. *)
+
   check_universes : bool;
   (** If [false] universe constraints are not checked *)
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 7a553700e8..391b139496 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -19,6 +19,7 @@ module RelDecl = Context.Rel.Declaration
 
 let safe_flags oracle = {
   check_guarded = true;
+  check_positive = true;
   check_universes = true;
   conv_oracle = oracle;
   share_reduction = true;
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index b0366d6ec0..aa3ef715db 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -546,7 +546,7 @@ let check_inductive env kn mie =
   (* First type-check the inductive definition *)
   let (env_ar_par, univs, variance, record, paramsctxt, inds) = IndTyping.typecheck_inductive env mie in
   (* Then check positivity conditions *)
-  let chkpos = (Environ.typing_flags env).check_guarded in
+  let chkpos = (Environ.typing_flags env).check_positive in
   let names = Array.map_of_list (fun entry -> entry.mind_entry_typename, entry.mind_entry_consnames)
       mie.mind_entry_inds
   in
diff --git a/tactics/declare.ml b/tactics/declare.ml
index e093a27728..391524ebda 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -246,7 +246,7 @@ let get_roles export eff =
 let feedback_axiom () = Feedback.(feedback AddedAxiom)
 let is_unsafe_typing_flags () =
   let flags = Environ.typing_flags (Global.env()) in
-  not (flags.check_universes && flags.check_guarded)
+  not (flags.check_universes && flags.check_guarded && flags.check_positive)
 
 let define_constant ~side_effect ~name cd =
   let open Proof_global in
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index ab341e4ab8..cbdc84e073 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -329,7 +329,7 @@ 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_guarded then
+      if mind.mind_typing_flags.check_positive then
         accu
       else
         let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 23a8bf20a3..cf87646905 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -553,7 +553,7 @@ let declare_default_schemes kn =
   let mib = Global.lookup_mind kn in
   let n = Array.length mib.mind_packets in
   if !elim_flag && (mib.mind_finite <> Declarations.BiFinite || !bifinite_elim_flag)
-     && mib.mind_typing_flags.check_guarded then
+     && mib.mind_typing_flags.check_positive then
     declare_induction_schemes kn;
   if !case_flag then map_inductive_block declare_one_case_analysis_scheme kn n;
   if is_eq_flag() then try_declare_beq_scheme kn;
-- 
cgit v1.2.3


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 +++++
 printing/printer.mli    | 2 ++
 vernac/g_vernac.mlg     | 1 +
 vernac/ppvernac.ml      | 2 ++
 vernac/vernacentries.ml | 1 +
 vernac/vernacexpr.ml    | 1 +
 6 files changed, 12 insertions(+)

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
diff --git a/printing/printer.mli b/printing/printer.mli
index a72f319636..0855f2d109 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -207,3 +207,5 @@ val pr_assumptionset : env -> evar_map -> types ContextObjectMap.t -> Pp.t
 
 val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t
 val pr_goal_emacs : proof:Proof.t option -> int -> int -> Pp.t
+
+val pr_typing_flags : Declarations.typing_flags -> Pp.t
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index dcd1979a85..fdf43196b0 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -1035,6 +1035,7 @@ GRAMMAR EXTEND Gram
       | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr
          -> { PrintCoercionPaths (s,t) }
       | IDENT "Canonical"; IDENT "Projections" -> { PrintCanonicalConversions }
+      | IDENT "Typing"; IDENT "Flags" -> { PrintTypingFlags }
       | IDENT "Tables" -> { PrintTables }
       | IDENT "Options" -> { PrintTables (* A Synonymous to Tables *) }
       | IDENT "Hint" -> { PrintHintGoal }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 0eb0b1b6f6..873a119e39 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -514,6 +514,8 @@ let string_of_theorem_kind = let open Decls in function
       ++ pr_class_rawexpr t
     | PrintCanonicalConversions ->
       keyword "Print Canonical Structures"
+    | PrintTypingFlags ->
+      keyword "Print Typing Flags"
     | PrintTables ->
       keyword "Print Tables"
     | PrintHintGoal ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index bc51dd46f3..4fb0129236 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1928,6 +1928,7 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt =
 let vernac_print ~pstate ~atts =
   let sigma, env = get_current_or_global_context ~pstate in
   function
+  | PrintTypingFlags -> pr_typing_flags (Environ.typing_flags (Global.env ()))
   | PrintTables -> print_tables ()
   | PrintFullContext-> print_full_context_typ env sigma
   | PrintSectionContext qid -> print_sec_context_typ env sigma qid
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 0968632c2d..c15baf6157 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -24,6 +24,7 @@ type goal_reference =
   | GoalId of Id.t
 
 type printable =
+  | PrintTypingFlags
   | PrintTables
   | PrintFullContext
   | PrintSectionContext of qualid
-- 
cgit v1.2.3


From abab878b8d8b5ca85a4da688abed68518f0b17bd Mon Sep 17 00:00:00 2001
From: SimonBoulier
Date: Wed, 14 Nov 2018 16:07:38 +0100
Subject: Set/Unset commands for typing flags

---
 kernel/environ.ml       |  2 ++
 kernel/safe_typing.ml   | 12 ++++++++++++
 kernel/safe_typing.mli  |  3 +++
 library/global.ml       |  3 +++
 library/global.mli      |  3 +++
 vernac/vernacentries.ml | 24 ++++++++++++++++++++++++
 6 files changed, 47 insertions(+)

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 9a75f0b682..1b17e954b7 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -418,6 +418,7 @@ let set_engagement c env = (* Unsafe *)
 (* It's convenient to use [{flags with foo = bar}] so we're smart wrt to it. *)
 let same_flags {
      check_guarded;
+     check_positive;
      check_universes;
      conv_oracle;
      indices_matter;
@@ -426,6 +427,7 @@ let same_flags {
      enable_native_compiler;
   } alt =
   check_guarded == alt.check_guarded &&
+  check_positive == alt.check_positive &&
   check_universes == alt.check_universes &&
   conv_oracle == alt.conv_oracle &&
   indices_matter == alt.indices_matter &&
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ea45f699ce..6970a11e72 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -194,6 +194,18 @@ let set_typing_flags c senv =
   if env == senv.env then senv
   else { senv with env }
 
+let set_check_guarded b senv =
+  let flags = Environ.typing_flags senv.env in
+  set_typing_flags { flags with check_guarded = b } senv
+
+let set_check_positive b senv =
+  let flags = Environ.typing_flags senv.env in
+  set_typing_flags { flags with check_positive = b } senv
+
+let set_check_universes b senv =
+  let flags = Environ.typing_flags senv.env in
+  set_typing_flags { flags with check_universes = b } senv
+
 let set_indices_matter indices_matter senv =
   set_typing_flags { (Environ.typing_flags senv.env) with indices_matter } senv
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 2406b6add1..fa53fa33fa 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -130,6 +130,9 @@ val set_engagement : Declarations.engagement -> safe_transformer0
 val set_indices_matter : bool -> safe_transformer0
 val set_typing_flags : Declarations.typing_flags -> safe_transformer0
 val set_share_reduction : bool -> safe_transformer0
+val set_check_guarded : bool -> safe_transformer0
+val set_check_positive : bool -> safe_transformer0
+val set_check_universes : bool -> safe_transformer0
 val set_VM : bool -> safe_transformer0
 val set_native_compiler : bool -> safe_transformer0
 val make_sprop_cumulative : safe_transformer0
diff --git a/library/global.ml b/library/global.ml
index ca774dbd74..0fc9e11364 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -89,6 +89,9 @@ let push_context_set b c = globalize0 (Safe_typing.push_context_set b c)
 let set_engagement c = globalize0 (Safe_typing.set_engagement c)
 let set_indices_matter b = globalize0 (Safe_typing.set_indices_matter b)
 let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c)
+let set_check_guarded c = globalize0 (Safe_typing.set_check_guarded c)
+let set_check_positive c = globalize0 (Safe_typing.set_check_positive c)
+let set_check_universes c = globalize0 (Safe_typing.set_check_universes c)
 let typing_flags () = Environ.typing_flags (env ())
 let make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative
 let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b)
diff --git a/library/global.mli b/library/global.mli
index d034bc4208..b089b7dd80 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -31,6 +31,9 @@ val named_context : unit -> Constr.named_context
 val set_engagement : Declarations.engagement -> unit
 val set_indices_matter : bool -> unit
 val set_typing_flags : Declarations.typing_flags -> unit
+val set_check_guarded : bool -> unit
+val set_check_positive : bool -> unit
+val set_check_universes : bool -> unit
 val typing_flags : unit -> Declarations.typing_flags
 val make_sprop_cumulative : unit -> unit
 val set_allow_sprop : bool -> unit
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4fb0129236..f90439d222 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1724,6 +1724,30 @@ let () =
       optread  = Nativenorm.get_profiling_enabled;
       optwrite = Nativenorm.set_profiling_enabled }
 
+let _ =
+  declare_bool_option
+    { optdepr  = false;
+      optname  = "guard checking";
+      optkey   = ["Guard"; "Checking"];
+      optread  = (fun () -> (Global.typing_flags ()).Declarations.check_guarded);
+      optwrite = (fun b -> Global.set_check_guarded b) }
+
+let _ =
+  declare_bool_option
+    { optdepr  = false;
+      optname  = "positivity/productivity checking";
+      optkey   = ["Positivity"; "Checking"];
+      optread  = (fun () -> (Global.typing_flags ()).Declarations.check_positive);
+      optwrite = (fun b -> Global.set_check_positive b) }
+
+let _ =
+  declare_bool_option
+    { optdepr  = false;
+      optname  = "universes checking";
+      optkey   = ["Universes"; "Checking"];
+      optread  = (fun () -> (Global.typing_flags ()).Declarations.check_universes);
+      optwrite = (fun b -> Global.set_check_universes b) }
+
 let vernac_set_strategy ~local l =
   let local = Option.default false local in
   let glob_ref r =
-- 
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 +++++--
 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


From 6414a2a96f6d9a237baf08b7b449a55ee5d34376 Mon Sep 17 00:00:00 2001
From: SimonBoulier
Date: Thu, 15 Nov 2018 09:42:08 +0100
Subject: Add a file for typing_flags in the test-suite.

---
 test-suite/success/typing_flags.v | 38 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 38 insertions(+)
 create mode 100644 test-suite/success/typing_flags.v

diff --git a/test-suite/success/typing_flags.v b/test-suite/success/typing_flags.v
new file mode 100644
index 0000000000..31550b45a6
--- /dev/null
+++ b/test-suite/success/typing_flags.v
@@ -0,0 +1,38 @@
+
+Print Typing Flags.
+Unset Guard Checking.
+Fixpoint f' (n : nat) : nat := f' n.
+
+Fixpoint f (n : nat) : nat.
+Proof.
+  exact (f n).
+Defined.
+
+Fixpoint bla (A:Type) (n:nat) := match n with 0 =>0 | S n => n end.
+
+Print Typing Flags.
+
+Set Guard Checking.
+
+Print Assumptions f.
+
+Unset Universes Checking.
+
+Definition T := Type.
+Fixpoint g (n : nat) : T := T.
+
+Print Typing Flags.
+Set Universes Checking.
+
+Fail Definition g2 (n : nat) : T := T.
+
+Fail Definition e := fix e (n : nat) : nat := e n.
+
+Unset Positivity Checking.
+
+Inductive Cor :=
+| Over : Cor
+| Next : ((Cor -> list nat) -> list nat) -> Cor.
+
+Set Positivity Checking.
+Print Assumptions Cor.
-- 
cgit v1.2.3


From de02e40124e4938fd4796303b8f5686e542fcb1a Mon Sep 17 00:00:00 2001
From: SimonBoulier
Date: Thu, 15 Nov 2018 12:12:58 +0100
Subject: Add documentation for typing flags.

---
 .../07-commands-and-options/10291-typing-flags.rst |  4 ++
 .../language/gallina-specification-language.rst    |  3 +-
 doc/sphinx/proof-engine/vernacular-commands.rst    | 73 ++++++++++++++++++++++
 3 files changed, 79 insertions(+), 1 deletion(-)
 create mode 100644 doc/changelog/07-commands-and-options/10291-typing-flags.rst

diff --git a/doc/changelog/07-commands-and-options/10291-typing-flags.rst b/doc/changelog/07-commands-and-options/10291-typing-flags.rst
new file mode 100644
index 0000000000..ef7adde801
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/10291-typing-flags.rst
@@ -0,0 +1,4 @@
+- Adding unsafe commands to enable/disable guard checking, positivity checking
+  and universes checking (providing a local `-type-in-type`).
+  See :ref:`controlling-typing-flags`.
+  (`#10291 <https://github.com/coq/coq/pull/10291>`_ by Simon Boulier).
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 91dfa34494..2cbd41af8b 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -778,7 +778,8 @@ Simple inductive types
 
       The types of the constructors have to satisfy a *positivity condition*
       (see Section :ref:`positivity`). This condition ensures the soundness of
-      the inductive definition.
+      the inductive definition. The positivity checking can be disabled using
+      the option :flag:`Positivity Checking` (see :ref:`controlling-typing-flags`).
 
    .. exn:: The conclusion of @type is not valid; it must be built from @ident.
 
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 774732825a..8d7bf78a85 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1204,6 +1204,79 @@ Controlling the locality of commands
      occurs in a section.  The :cmd:`Set` and :cmd:`Unset` commands belong to this
      category.
 
+.. _controlling-typing-flags:
+
+Controlling Typing Flags
+----------------------------
+
+.. flag:: Guard Checking
+
+   This option can be used to enable/disable the guard checking of
+   fixpoints. Warning: this can break the consistency of the system, use at your
+   own risk. Decreasing argument can still be specified: the decrease is not checked
+   anymore but it still affects the reduction of the term. Unchecked fixpoints are
+   printed by :cmd:`Print Assumptions`.
+
+.. flag:: Positivity Checking
+
+   This option can be used to enable/disable the positivity checking of inductive
+   types and the productivity checking of coinductive types. Warning: this can
+   break the consistency of the system, use at your own risk. Unchecked
+   (co)inductive types are printed by :cmd:`Print Assumptions`.
+
+.. flag:: Universes Checking
+
+   This option can be used to enable/disable the checking of universes, providing a
+   form of "type in type".  Warning: this breaks the consistency of the system, use
+   at your own risk.  Constants relying on "type in type" are printed by
+   :cmd:`Print Assumptions`. It has the same effect as `-type-in-type` command line
+   argument (see :ref:`command-line-options`).
+
+.. cmd:: Print Typing Flags
+
+   Print the status of the three typing flags: guard checking, positivity checking
+   and universe checking.
+
+.. example::
+
+   .. coqtop:: all reset
+
+        Unset Guard Checking.
+
+        Print Typing Flags.
+
+        Fixpoint f (n : nat) : False
+          := f n.
+
+        Fixpoint ackermann (m n : nat) {struct m} : nat :=
+          match m with
+          | 0 => S n
+          | S m =>
+            match n with
+            | 0 => ackermann m 1
+            | S n => ackermann m (ackermann (S m) n)
+            end
+          end.
+
+        Print Assumptions ackermann.
+
+   Note that the proper way to define the Ackermann function is to use
+   an inner fixpoint:
+
+   .. coqtop:: all reset
+
+        Fixpoint ack m :=
+          fix ackm n :=
+          match m with
+          | 0 => S n
+          | S m' =>
+            match n with
+            | 0 => ack m' 1
+            | S n' => ack m' (ackm n')
+            end
+          end.
+
+
 .. _internal-registration-commands:
 
 Internal registration commands
-- 
cgit v1.2.3


From 24701948804ecdc7c2518773fd66308913441195 Mon Sep 17 00:00:00 2001
From: SimonBoulier
Date: Mon, 3 Jun 2019 17:17:35 +0200
Subject: Universe Checking instead of Universes Checking

---
 doc/sphinx/proof-engine/vernacular-commands.rst | 2 +-
 test-suite/success/typing_flags.v               | 4 ++--
 vernac/vernacentries.ml                         | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 8d7bf78a85..c391cc949d 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1224,7 +1224,7 @@ Controlling Typing Flags
    break the consistency of the system, use at your own risk. Unchecked
    (co)inductive types are printed by :cmd:`Print Assumptions`.
 
-.. flag:: Universes Checking
+.. flag:: Universe Checking
 
    This option can be used to enable/disable the checking of universes, providing a
    form of "type in type".  Warning: this breaks the consistency of the system, use
diff --git a/test-suite/success/typing_flags.v b/test-suite/success/typing_flags.v
index 31550b45a6..c15701e000 100644
--- a/test-suite/success/typing_flags.v
+++ b/test-suite/success/typing_flags.v
@@ -16,13 +16,13 @@ Set Guard Checking.
 
 Print Assumptions f.
 
-Unset Universes Checking.
+Unset Universe Checking.
 
 Definition T := Type.
 Fixpoint g (n : nat) : T := T.
 
 Print Typing Flags.
-Set Universes Checking.
+Set Universe Checking.
 
 Fail Definition g2 (n : nat) : T := T.
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index f90439d222..8712b8e958 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1744,7 +1744,7 @@ let _ =
   declare_bool_option
     { optdepr  = false;
       optname  = "universes checking";
-      optkey   = ["Universes"; "Checking"];
+      optkey   = ["Universe"; "Checking"];
       optread  = (fun () -> (Global.typing_flags ()).Declarations.check_universes);
       optwrite = (fun b -> Global.set_check_universes b) }
 
-- 
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 +++++++++++++++++-----------
 printing/printer.mli              |  4 ++--
 test-suite/success/typing_flags.v |  5 +++++
 vernac/assumptions.ml             | 32 +++++++++++++++++++++++---------
 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
-- 
cgit v1.2.3


From d6d8229dd8d71cf8cac1d116426bf772a9b8821b Mon Sep 17 00:00:00 2001
From: SimonBoulier
Date: Fri, 7 Jun 2019 14:16:41 +0200
Subject: Fix typing_flags in the checker

Now all relevant typing_flags are taken in account by the checker.
The different forms of assumptions are now printed by the checker.
---
 checker/checkInductive.ml |  8 ++++++--
 checker/check_stat.ml     | 32 ++++++++++++++++++++++++++------
 checker/mod_checking.ml   | 13 ++++++++-----
 kernel/environ.ml         |  3 +++
 kernel/environ.mli        |  1 +
 5 files changed, 44 insertions(+), 13 deletions(-)

diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index f2df99dcd6..d20eea7874 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -142,8 +142,12 @@ let check_inductive env mind mb =
         mind_universes; mind_variance;
         mind_private; mind_typing_flags; }
     =
-    (* Locally set the oracle for further typechecking *)
-    let env = Environ.set_oracle env mb.mind_typing_flags.conv_oracle in
+    (* Locally set typing flags for further typechecking *)
+    let mb_flags = mb.mind_typing_flags in
+    let env = Environ.set_typing_flags {env.env_typing_flags with check_guarded = mb_flags.check_guarded;
+                                                                  check_positive = mb_flags.check_positive;
+                                                                  check_universes = mb_flags.check_universes;
+                                                                  conv_oracle = mb_flags.conv_oracle} env in
     Indtypes.check_inductive env mind entry
   in
   let check = check mind in
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 62f72c8edc..a67945ae94 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -31,14 +31,31 @@ let pr_engagement env =
     | PredicativeSet -> str "Theory: Set is predicative"
   end
 
-let is_ax _ cb = not (Declareops.constant_has_body cb)
 
-let pr_ax env =
-  let axs = fold_constants (fun c ce acc -> if is_ax c ce then c::acc else acc) env [] in
+let pr_assumptions ass axs =
   if axs = [] then
-    str "Axioms: <none>"
+    str ass ++ str ": <none>"
   else
-    hv 2 (str "Axioms:" ++ fnl() ++ prlist_with_sep fnl Constant.print axs)
+    hv 2 (str ass ++ str ":" ++ fnl() ++ prlist_with_sep fnl str axs)
+
+let pr_axioms env =
+  let csts = fold_constants (fun c cb acc -> if not (Declareops.constant_has_body cb) then Constant.to_string c :: acc else acc) env [] in
+  pr_assumptions "Axioms" csts
+
+let pr_type_in_type env =
+  let csts = fold_constants (fun c cb acc -> if not cb.const_typing_flags.check_universes then Constant.to_string c :: acc else acc) env [] in
+  let csts = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_universes then MutInd.to_string c :: acc else acc) env csts in
+  pr_assumptions "Constants/Inductives relying on type-in-type" csts
+
+let pr_unguarded env =
+  let csts = fold_constants (fun c cb acc -> if not cb.const_typing_flags.check_guarded then Constant.to_string c :: acc else acc) env [] in
+  let csts = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_guarded then MutInd.to_string c :: acc else acc) env csts in
+  pr_assumptions "Constants/Inductives relying on unsafe (co)fixpoints" csts
+
+let pr_nonpositive env =
+  let inds = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_positive then MutInd.to_string c :: acc else acc) env [] in
+  pr_assumptions "Inductives whose positivity is assumed" inds
+
 
 let print_context env =
   if !output_context then begin
@@ -47,7 +64,10 @@ let print_context env =
       (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
       str"===============" ++ fnl() ++ fnl() ++
       str "* " ++ hov 0 (pr_engagement env ++ fnl()) ++ fnl() ++
-      str "* " ++ hov 0 (pr_ax env)));
+      str "* " ++ hov 0 (pr_axioms env ++ fnl()) ++ fnl() ++
+      str "* " ++ hov 0 (pr_type_in_type env ++ fnl()) ++ fnl() ++
+      str "* " ++ hov 0 (pr_unguarded env ++ fnl()) ++ fnl() ++
+      str "* " ++ hov 0 (pr_nonpositive env)))
   end
 
 let stats env =
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 9b41fbcb7a..09b8c48c15 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -17,9 +17,12 @@ let set_indirect_accessor f = indirect_accessor := f
 
 let check_constant_declaration env kn cb =
   Flags.if_verbose Feedback.msg_notice (str "  checking cst:" ++ Constant.print kn);
-  (* Locally set the oracle for further typechecking *)
-  let oracle = env.env_typing_flags.conv_oracle in
-  let env = Environ.set_oracle env cb.const_typing_flags.conv_oracle in
+  (* Locally set typing flags for further typechecking *)
+  let orig_flags = env.env_typing_flags in
+  let cb_flags = cb.const_typing_flags in
+  let env = Environ.set_typing_flags {orig_flags with check_guarded = cb_flags.check_guarded;
+                                                      check_universes = cb_flags.check_universes;
+                                                      conv_oracle = cb_flags.conv_oracle} env in
   (* [env'] contains De Bruijn universe variables *)
   let poly, env' =
     match cb.const_universes with
@@ -57,8 +60,8 @@ let check_constant_declaration env kn cb =
     if poly then add_constant kn cb env
     else add_constant kn cb env'
   in
-  (* Reset the value of the oracle *)
-  Environ.set_oracle env oracle
+  (* Reset the value of the typing flags *)
+  Environ.set_typing_flags orig_flags env
 
 (** {6 Checking modules } *)
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 1b17e954b7..655094e88b 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -216,6 +216,9 @@ let lookup_named_ctxt id ctxt =
 let fold_constants f env acc =
   Cmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_constants acc
 
+let fold_inductives f env acc =
+  Mindmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_inductives acc
+
 (* Global constants *)
 
 let lookup_constant_key kn env =
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 6cd4f96645..e6d814ac7d 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -176,6 +176,7 @@ val pop_rel_context : int -> env -> env
 
 (** Useful for printing *)
 val fold_constants : (Constant.t -> Opaqueproof.opaque constant_body -> 'a -> 'a) -> env -> 'a -> 'a
+val fold_inductives : (MutInd.t -> Declarations.mutual_inductive_body -> 'a -> 'a) -> env -> 'a -> 'a
 
 (** {5 Global constants }
   {6 Add entries to global environment } *)
-- 
cgit v1.2.3