diff options
| author | Maxime Dénès | 2019-04-05 10:10:16 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-10 15:41:44 +0200 |
| commit | 4d1cbe175e3f235c143061796b919b03d933f00a (patch) | |
| tree | 8da23f5ab428941659eec5342255ab6f79460ed2 /pretyping/typing.ml | |
| parent | 84fa6a47a7ca5fbb5c83595ea2491f821b0c9d86 (diff) | |
Remove calls to Global.env in Typing
Diffstat (limited to 'pretyping/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 89f72c874b..be71f44a5e 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 |