diff options
Diffstat (limited to 'pretyping/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 0bb2979c2..fa6fd9677 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) -> |