diff options
| author | Pierre-Marie Pédrot | 2016-06-18 20:07:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-18 20:07:02 +0200 |
| commit | b2495b2326083776f9b15355acac77cde73545e1 (patch) | |
| tree | d030b2e5fbd6fe9c7bba68e5fb80d2546ab96f92 /kernel/inductive.ml | |
| parent | 561dbba4ce47aa1920b27a6fa3ea1fdb03835557 (diff) | |
| parent | 371d69b334837c51d0dc998ddefbd072ac8dde2f (diff) | |
Merge PR# 169: Local type-in-type flag.
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 24bdaa5c43..8e26370ecf 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 |