Merge PR #8694: Various cleanups of universe apis

1 files changed, 26 insertions, 22 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 2fa33eb1cd..3b7e3ae544 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -419,12 +419,6 @@ let constant_type env (kn,u) =
     let csts = constraints_of cb u in
     (subst_instance_constr u cb.const_type, csts)
 
-let constant_context env kn =
-  let cb = lookup_constant kn env in
-  match cb.const_universes with
-  | Monomorphic_const _ -> Univ.AUContext.empty
-  | Polymorphic_const ctx -> ctx
-
 type const_evaluation_result = NoBody | Opaque
 
 exception NotEvaluableConst of const_evaluation_result
@@ -550,28 +544,38 @@ let lookup_inductive_variables (kn,_i) env =
 let lookup_constructor_variables (ind,_) env =
   lookup_inductive_variables ind env
 
+(* Universes *)
+let constant_context env c =
+  let cb = lookup_constant c env in
+  Declareops.constant_polymorphic_context cb
+
+let universes_of_global env r =
+  let open GlobRef in
+    match r with
+    | VarRef _ -> Univ.AUContext.empty
+    | ConstRef c -> constant_context env c
+    | 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 =
-  match kind constr with
-      Var id -> Id.Set.singleton id
-    | Const (kn, _) -> lookup_constant_variables kn env
-    | Ind (ind, _) -> lookup_inductive_variables ind env
-    | Construct (cstr, _) -> lookup_constructor_variables cstr env
-    (** FIXME: is Proj missing? *)
-    | _ -> raise Not_found
+let vars_of_global env gr =
+  let open GlobRef in
+  match gr with
+  | VarRef id -> Id.Set.singleton id
+  | ConstRef kn -> lookup_constant_variables kn env
+  | IndRef ind -> lookup_inductive_variables ind env
+  | ConstructRef cstr -> lookup_constructor_variables cstr env
 
 let global_vars_set env constr =
   let rec filtrec acc c =
-    let acc =
-      match kind c with
-      | Var _ | Const _ | Ind _ | Construct _ ->
-	  Id.Set.union (vars_of_global env c) acc
-      | _ ->
-	  acc in
-    Constr.fold filtrec acc c
+    match destRef c with
+    | gr, _ ->
+      Id.Set.union (vars_of_global env gr) acc
+    | exception DestKO -> Constr.fold filtrec acc c
   in
-    filtrec Id.Set.empty constr
+  filtrec Id.Set.empty constr
 
 
 (* [keep_hyps env ids] keeps the part of the section context of [env] which