From 6a7bcfc6d22ab3bf38847fa3fd05ec194187ff50 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Oct 2018 12:56:47 +0200
Subject: Deprecate Global.universes_of_global (replaced by environ version)

---
 kernel/environ.ml  | 12 ++++++++++++
 kernel/environ.mli |  2 ++
 2 files changed, 14 insertions(+)

(limited to 'kernel')

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
-- 
cgit v1.2.3