diff options
Diffstat (limited to 'library/global.ml')
| -rw-r--r-- | library/global.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/library/global.ml b/library/global.ml index 65e895dfd..adfb7cafe 100644 --- a/library/global.ml +++ b/library/global.ml @@ -152,7 +152,9 @@ let type_of_global_unsafe r = | VarRef id -> Environ.named_type id env | ConstRef c -> let cb = Environ.lookup_constant c env in - Typeops.type_of_constant_type env cb.Declarations.const_type + let univs = Declareops.universes_of_polymorphic_constant cb in + let ty = Typeops.type_of_constant_type env cb.Declarations.const_type in + Vars.subst_instance_constr (Univ.UContext.instance univs) ty | IndRef ind -> let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in let inst = @@ -195,7 +197,7 @@ let universes_of_global env r = | VarRef id -> Univ.UContext.empty | ConstRef c -> let cb = Environ.lookup_constant c env in - Declareops.universes_of_constant cb + Declareops.universes_of_polymorphic_constant cb | IndRef ind -> let (mib, oib) = Inductive.lookup_mind_specif env ind in Univ.instantiate_univ_context mib.mind_universes |