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 /kernel/inductive.ml | |
| parent | 806e3bc0ecfbf0a6bfd20e80caa8250e60d39152 (diff) | |
Moving the typing_flags to the environment.
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 |