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 efea4bec89..930b0413e5 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -593,9 +593,9 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty = let control_only_guard env c = let check_fix_cofix e c = match kind_of_term c with | CoFix (_,(_,_,_) as cofix) -> - Inductive.check_cofix ~chk:true e cofix + Inductive.check_cofix ~flags:{check_guarded=true} e cofix | Fix (_,(_,_,_) as fix) -> - Inductive.check_fix ~chk:true e fix + Inductive.check_fix ~flags:{check_guarded=true} e fix | _ -> () in let rec iter env c = diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index d9f490ba55..8fbcc8e5e7 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -75,7 +75,7 @@ let search_guard loc env possible_indexes fixdefs = if List.for_all is_singleton possible_indexes then let indexes = Array.of_list (List.map List.hd possible_indexes) in let fix = ((indexes, 0),fixdefs) in - (try check_fix env ~chk:true fix + (try check_fix env ~flags:{Declarations.check_guarded=true} fix with reraise -> let (e, info) = Errors.push reraise in let info = Loc.add_loc info loc in @@ -88,7 +88,7 @@ let search_guard loc env possible_indexes fixdefs = (fun l -> let indexes = Array.of_list l in let fix = ((indexes, 0),fixdefs) in - try check_fix env ~chk:true fix; raise (Found indexes) + try check_fix env ~flags:{Declarations.check_guarded=true} fix; raise (Found indexes) with TypeError _ -> ()) (List.combinations possible_indexes); let errmsg = "Cannot guess decreasing argument of fix." in @@ -537,7 +537,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | GCoFix i -> let cofix = (i,(names,ftys,fdefs)) in - (try check_cofix env ~chk:true cofix + (try check_cofix env ~flags:{Declarations.check_guarded=true} 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 0bb2979c2a..fa6fd9677b 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -184,13 +184,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 ~chk:true fix; + check_fix env ~flags:{Declarations.check_guarded=true} 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 ~chk:true cofix; + check_cofix env ~flags:{Declarations.check_guarded=true} cofix; make_judge (mkCoFix cofix) tys.(i) | Sort (Prop c) -> |