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 f03e6c6e9..52afa7f83 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:Declareops.safe_flags fix; + check_fix env 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:Declareops.safe_flags cofix; + check_cofix env cofix; make_judge (mkCoFix cofix) tys.(i) | Sort (Prop c) -> |