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).

---
 vernac/assumptions.ml | 2 +-
 vernac/indschemes.ml  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac')

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