diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 14 | ||||
| -rw-r--r-- | library/global.mli | 1 |
2 files changed, 1 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 diff --git a/library/global.mli b/library/global.mli index fd6c9a60d4..29255a70ff 100644 --- a/library/global.mli +++ b/library/global.mli @@ -143,6 +143,7 @@ val type_of_global_in_context : Environ.env -> (** Returns the universe context of the global reference (whatever its polymorphic status is). *) val universes_of_global : GlobRef.t -> Univ.AUContext.t +[@@ocaml.deprecated "Use [Environ.universes_of_global]"] (** {6 Retroknowledge } *) |