diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-17 18:25:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-18 18:54:43 +0200 |
| commit | 53ced0735f7e24735d78a02fc74588b8d9186eab (patch) | |
| tree | 93661920f42d9be934e59f5f972d165ea24785b7 /pretyping/typing.ml | |
| parent | 806e3bc0ecfbf0a6bfd20e80caa8250e60d39152 (diff) | |
Moving the typing_flags to the environment.
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) -> |