diff options
| author | Hugo Herbelin | 2018-10-09 20:22:59 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-19 16:52:55 +0200 |
| commit | df6b72e348543a289a2ef3f89f32c905add564bc (patch) | |
| tree | 3fc74e3474457f12a9cd4975707c67553b3e6db1 /library/global.ml | |
| parent | 988aab80e03e593c76869b113c5bcc043209d952 (diff) | |
Moving Global.type_of_global_in_context to Typeops.
It is purely functional, so no need for it to be in global now that
GlobRef.t are in the kernel.
Also updated the comments.
Diffstat (limited to 'library/global.ml')
| -rw-r--r-- | library/global.ml | 21 |
1 files changed, 1 insertions, 20 deletions
diff --git a/library/global.ml b/library/global.ml index 1ad72afea1..1672d508c2 100644 --- a/library/global.ml +++ b/library/global.ml @@ -189,26 +189,7 @@ let constr_of_global_in_context env r = let univs = Declareops.inductive_polymorphic_context mib in mkConstructU (cstr, Univ.make_abstract_instance univs), univs -let type_of_global_in_context env r = - match r with - | VarRef id -> Environ.named_type id env, Univ.AUContext.empty - | ConstRef c -> - let cb = Environ.lookup_constant c env in - let univs = Declareops.constant_polymorphic_context cb in - cb.Declarations.const_type, univs - | IndRef ind -> - let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in - let univs = Declareops.inductive_polymorphic_context mib in - let inst = Univ.make_abstract_instance univs in - let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in - Inductive.type_of_inductive env (specif, inst), univs - | ConstructRef cstr -> - let (mib,oib as specif) = - Inductive.lookup_mind_specif env (inductive_of_constructor cstr) - in - let univs = Declareops.inductive_polymorphic_context mib in - let inst = Univ.make_abstract_instance univs in - Inductive.type_of_constructor (cstr,inst) specif, univs +let type_of_global_in_context = Typeops.type_of_global_in_context let universes_of_global gr = universes_of_global (env ()) gr |