Merge PR #6425: Cleanup universes in the kernel

4 files changed, 8 insertions, 15 deletions

diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index d59102b6c7..8ac471404a 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -40,16 +40,10 @@ let subst_rename_args (subst, (_, (r, names as orig))) =
   let r' = fst (subst_global subst r) in 
   if r==r' then orig else (r', names)
 
-let section_segment_of_reference = function
-  | ConstRef con -> Lib.section_segment_of_constant con
-  | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
-      Lib.section_segment_of_mutual_inductive kn
-  | _ -> [], Univ.LMap.empty, Univ.AUContext.empty
-
 let discharge_rename_args = function
   | _, (ReqGlobal (c, names), _ as req) ->
      (try 
-       let vars,_,_ = section_segment_of_reference c in
+       let vars = Lib.variable_section_segment_of_reference c in
        let c' = pop_global_reference c in
        let var_names = List.map (fst %> NamedDecl.get_id %> Name.mk_name) vars in
        let names' = var_names @ names in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index ac88468545..78de0437d0 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -121,10 +121,10 @@ module ReductionBehaviour = struct
     let r' = fst (subst_global subst r) in if r==r' then orig else (r',o)
 
   let discharge = function
-    | _,(ReqGlobal (ConstRef c, req), (_, b)) ->
+    | _,(ReqGlobal (ConstRef c as gr, req), (_, b)) ->
       let b =
-        if Lib.is_in_section (ConstRef c) then
-          let vars, _, _ = Lib.section_segment_of_constant c in
+        if Lib.is_in_section gr then
+          let vars = Lib.variable_section_segment_of_reference gr in
           let extra = List.length vars in
           let nargs' =
              if b.b_nargs = max_int then max_int
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index f153b63410..3f947fd23f 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -219,7 +219,8 @@ let discharge_class (_,cl) =
     in grs', discharge_rel_context subst 1 ctx @ ctx' in
   let cl_impl' = Lib.discharge_global cl.cl_impl in
   if cl_impl' == cl.cl_impl then cl else
-    let ctx, _, _ as info = abs_context cl in
+    let info = abs_context cl in
+    let ctx = info.Lib.abstr_ctx in
     let ctx, subst = rel_of_variable_context ctx in
     let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in
     let context = discharge_context ctx (subst, usubst) cl.cl_context in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index b41fb4e4dd..8df8f84742 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-module CVars = Vars
-
 open CErrors
 open Pp
 open Util
@@ -1527,7 +1525,7 @@ let indirectly_dependent sigma c d decls =
 let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) =
   let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in
   let sigma, subst = nf_univ_variables sigma in
-  (sigma, EConstr.of_constr (CVars.subst_univs_constr subst (EConstr.Unsafe.to_constr (nf_evar sigma c))))
+  (sigma, EConstr.of_constr (Universes.subst_univs_constr subst (EConstr.Unsafe.to_constr (nf_evar sigma c))))
 
 let default_matching_core_flags sigma =
   let ts = Names.full_transparent_state in {
@@ -1617,7 +1615,7 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
   | Some (sigma,_,l) ->
      let c = applist (nf_evar sigma (local_strong whd_meta sigma c), l) in
      let univs, subst = nf_univ_variables sigma in
-     Some (sigma,EConstr.of_constr (CVars.subst_univs_constr subst (EConstr.Unsafe.to_constr c))))
+     Some (sigma,EConstr.of_constr (Universes.subst_univs_constr subst (EConstr.Unsafe.to_constr c))))
 
 let make_eq_test env evd c =
   let out cstr =