diff options
| author | Pierre-Marie Pédrot | 2018-10-17 15:29:47 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-17 15:29:47 +0200 |
| commit | 15998894ff76b1fa9354085ea0bddae4f8f23ddf (patch) | |
| tree | 254cc3a53b6aa344f49a10cba32e14acf97d2905 /library | |
| parent | 063cf49f40511730c8c60c45332e92823ce4c78f (diff) | |
| parent | 6aa0aa37e19457a8c0c3ad36f7bbead058442344 (diff) | |
Merge PR #8694: Various cleanups of universe apis
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 } *) |