diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-20 20:45:32 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-20 20:56:47 +0100 |
| commit | 7bbbb3f354a71e7416f3c9ebbd351e192d54e63e (patch) | |
| tree | 3810037be4ea9ab4ff7d4f49105df98466a3136a /pretyping | |
| parent | 12c61c7ab522ea58bf8c5692de7130e124a2cc0a (diff) | |
Probably useless use of a global-environment reading function in Indrec.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/indrec.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index c1ac0d995..cce0ff5ec 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -538,13 +538,13 @@ let weaken_sort_scheme env evd set sort npars term ty = (* Check inductive types only occurs once (otherwise we obtain a meaning less scheme) *) -let check_arities listdepkind = +let check_arities env listdepkind = let _ = List.fold_left (fun ln (((_,ni as mind),u),mibi,mipi,dep,kind) -> let kelim = elim_sorts (mibi,mipi) in if not (Sorts.List.mem kind kelim) then raise (RecursionSchemeError - (NotAllowedCaseAnalysis (true, fst (Universes.fresh_sort_in_family (Global.env ()) + (NotAllowedCaseAnalysis (true, fst (Universes.fresh_sort_in_family env kind),(mind,u)))) else if Int.List.mem ni ln then raise (RecursionSchemeError (NotMutualInScheme (mind,mind))) @@ -554,7 +554,7 @@ let check_arities listdepkind = let build_mutual_induction_scheme env sigma = function | ((mind,u),dep,s)::lrecspec -> - let (mib,mip) = Global.lookup_inductive mind in + let (mib,mip) = lookup_mind_specif env mind in let (sp,tyi) = mind in let listdepkind = ((mind,u),mib,mip,dep,s):: @@ -568,7 +568,7 @@ let build_mutual_induction_scheme env sigma = function raise (RecursionSchemeError (NotMutualInScheme (mind,mind')))) lrecspec) in - let _ = check_arities listdepkind in + let _ = check_arities env listdepkind in mis_make_indrec env sigma listdepkind mib u | _ -> anomaly (Pp.str "build_induction_scheme expects a non empty list of inductive types") |