diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/inductiveops.ml | 4 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 6 | ||||
| -rw-r--r-- | pretyping/typing.ml | 4 |
3 files changed, 7 insertions, 7 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 0b488308a1..1d77204543 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -592,9 +592,9 @@ let type_of_projection_knowing_arg env sigma p c ty = let control_only_guard env c = let check_fix_cofix e c = match kind_of_term c with | CoFix (_,(_,_,_) as cofix) -> - Inductive.check_cofix ~flags:{check_guarded=true} e cofix + Inductive.check_cofix ~flags:Declareops.safe_flags e cofix | Fix (_,(_,_,_) as fix) -> - Inductive.check_fix ~flags:{check_guarded=true} e fix + Inductive.check_fix ~flags:Declareops.safe_flags e fix | _ -> () in let rec iter env c = diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index c894d96a78..65f5b3fd0f 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -101,7 +101,7 @@ let search_guard ~tflags loc env possible_indexes fixdefs = will be chosen). A more robust solution may be to raise an error when totality is assumed but the strutural argument is not specified. *) - try check_fix env ~flags:{Declarations.check_guarded=true} fix; raise (Found indexes) + try check_fix env ~flags:Declareops.safe_flags fix; raise (Found indexes) with TypeError _ -> ()) (List.combinations possible_indexes); let errmsg = "Cannot guess decreasing argument of fix." in @@ -617,13 +617,13 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let fixdecls = (names,ftys,fdefs) in let indexes = search_guard - ~tflags:{Declarations.check_guarded=true} + ~tflags:Declareops.safe_flags loc env possible_indexes fixdecls in make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | GCoFix i -> let cofix = (i,(names,ftys,fdefs)) in - (try check_cofix env ~flags:{Declarations.check_guarded=true} cofix + (try check_cofix env ~flags:Declareops.safe_flags cofix with reraise -> let (e, info) = Errors.push reraise in let info = Loc.add_loc info loc in diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 598dd16d06..f03e6c6e96 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -189,13 +189,13 @@ let rec execute env evdref cstr = | Fix ((vn,i as vni),recdef) -> let (_,tys,_ as recdef') = execute_recdef env evdref recdef in let fix = (vni,recdef') in - check_fix env ~flags:{Declarations.check_guarded=true} fix; + check_fix env ~flags:Declareops.safe_flags fix; make_judge (mkFix fix) tys.(i) | CoFix (i,recdef) -> let (_,tys,_ as recdef') = execute_recdef env evdref recdef in let cofix = (i,recdef') in - check_cofix env ~flags:{Declarations.check_guarded=true} cofix; + check_cofix env ~flags:Declareops.safe_flags cofix; make_judge (mkCoFix cofix) tys.(i) | Sort (Prop c) -> |