diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 24bdaa5c4..8e26370ec 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1067,7 +1067,8 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = (Array.map fst rv, Array.map snd rv) -let check_fix env ~flags ((nvect,_),(names,_,bodies as recdef) as fix) = +let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) = + let flags = Environ.typing_flags env in if flags.check_guarded then let (minds, rdef) = inductive_of_mutfix env fix in let get_tree (kn,i) = @@ -1195,7 +1196,8 @@ let check_one_cofix env nbfix def deftype = (* The function which checks that the whole block of definitions satisfies the guarded condition *) -let check_cofix env ~flags (bodynum,(names,types,bodies as recdef)) = +let check_cofix env (bodynum,(names,types,bodies as recdef)) = + let flags = Environ.typing_flags env in if flags.check_guarded then let nbfix = Array.length bodies in for i = 0 to nbfix-1 do |