Split the [check_guarded] typing_flag into [check_guarded] (for (co)fixpoints) and [check_positive] (for (co)inductive types).

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;