diff options
| author | Gaëtan Gilbert | 2018-10-10 12:56:47 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-10-16 15:51:49 +0200 |
| commit | 6a7bcfc6d22ab3bf38847fa3fd05ec194187ff50 (patch) | |
| tree | 0185cd9dc7a9f6e3e9fa6fcca8b86e79a49a20c1 /library/global.ml | |
| parent | 096d4dd94ff6d506e7a3785da453c21874611cec (diff) | |
Deprecate Global.universes_of_global (replaced by environ version)
Diffstat (limited to 'library/global.ml')
| -rw-r--r-- | library/global.ml | 14 |
1 files changed, 0 insertions, 14 deletions
diff --git a/library/global.ml b/library/global.ml index 769a4bea38..1ad72afea1 100644 --- a/library/global.ml +++ b/library/global.ml @@ -210,20 +210,6 @@ let type_of_global_in_context env r = let inst = Univ.make_abstract_instance univs in Inductive.type_of_constructor (cstr,inst) specif, univs -let universes_of_global env r = - match r with - | VarRef id -> Univ.AUContext.empty - | ConstRef c -> - let cb = Environ.lookup_constant c env in - Declareops.constant_polymorphic_context cb - | IndRef ind -> - let (mib, oib) = Inductive.lookup_mind_specif env ind in - Declareops.inductive_polymorphic_context mib - | ConstructRef cstr -> - let (mib,oib) = - Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - Declareops.inductive_polymorphic_context mib - let universes_of_global gr = universes_of_global (env ()) gr |