From 53ced0735f7e24735d78a02fc74588b8d9186eab Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 17 Jun 2016 18:25:02 +0200 Subject: Moving the typing_flags to the environment. --- kernel/inductive.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'kernel/inductive.ml') 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 -- cgit v1.2.3