Deprecate Global.universes_of_global (replaced by environ version)

5 files changed, 16 insertions, 15 deletions

diff --git a/engine/univNames.ml b/engine/univNames.ml
index e89dcedb9c..a71f9c5736 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -86,7 +86,7 @@ let register_universe_binders ref ubinders =
       part of the code that depends on the internal representation of names in
       abstract contexts, but removing it requires quite a rework of the
       callers. *)
-  let univs = AUContext.instance (Global.universes_of_global ref) in
+  let univs = AUContext.instance (Environ.universes_of_global (Global.env()) ref) in
   let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in
   let map lvl =
     try LMap.find lvl revmap
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 2fa33eb1cd..1feb47d387 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -550,6 +550,18 @@ let lookup_inductive_variables (kn,_i) env =
 let lookup_constructor_variables (ind,_) env =
   lookup_inductive_variables ind env
 
+(* Universes *)
+let universes_of_global env r =
+  let open GlobRef in
+    match r with
+    | VarRef _ -> Univ.AUContext.empty
+    | ConstRef c ->
+      let cb = lookup_constant c env in
+      Declareops.constant_polymorphic_context cb
+    | IndRef (mind,_) | ConstructRef ((mind,_),_) ->
+      let mib = lookup_mind mind env in
+      Declareops.inductive_polymorphic_context mib
+
 (* Returns the list of global variables in a term *)
 
 let vars_of_global env constr =
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 031e7968d7..6e313faab0 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -267,6 +267,8 @@ val push_constraints_to_env : 'a Univ.constrained -> env -> env
 val set_engagement : engagement -> env -> env
 val set_typing_flags : typing_flags -> env -> env
 
+val universes_of_global : env -> GlobRef.t -> AUContext.t
+
 (** {6 Sets of referred section variables }
    [global_vars_set env c] returns the list of [id]'s occurring either
    directly as [Var id] in [c] or indirectly as a section variable
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 } *)