From 4d1cbe175e3f235c143061796b919b03d933f00a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maxime=20D=C3=A9n=C3=A8s?= Date: Fri, 5 Apr 2019 10:10:16 +0200 Subject: [PATCH] Remove calls to Global.env in Typing --- pretyping/typing.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 89f72c874bed..be71f44a5e47 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -198,7 +198,7 @@ let check_type_fixpoint ?loc env sigma lna lar vdefj = (* FIXME: might depend on the level of actual parameters!*) let check_allowed_sort env sigma ind c p = - let specif = Global.lookup_inductive (fst ind) in + let specif = lookup_mind_specif env (fst ind) in let sorts = elim_sorts specif in let pj = Retyping.get_judgment_of env sigma p in let _, s = splay_prod env sigma pj.uj_type in