diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/assumptions.ml | 2 | ||||
| -rw-r--r-- | vernac/indschemes.ml | 2 |
2 files changed, 2 insertions, 2 deletions
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; |