Merge PR #8694: Various cleanups of universe apis

4 files changed, 9 insertions, 8 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 09e2b8df45..3cf5e9bfdf 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -9,6 +9,7 @@
 (************************************************************************)
 
 (*i*)
+module CVars = Vars
 open Names
 open EConstr
 open Nametab
@@ -116,8 +117,8 @@ let instance_hook k info global imps ?hook cst =
 let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype =
   let kind = IsDefinition Instance in
   let sigma =
-    let levels = Univ.LSet.union (Univops.universes_of_constr termtype)
-                                 (Univops.universes_of_constr term) in
+    let levels = Univ.LSet.union (CVars.universes_of_constr termtype)
+                                 (CVars.universes_of_constr term) in
     Evd.restrict_universe_context sigma levels
   in
   let uctx = Evd.check_univ_decl ~poly sigma decl in
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 9497f2fb03..e990f0cd15 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -162,7 +162,7 @@ let do_assumptions kind nl l =
   let nf_evar c = EConstr.to_constr sigma c in
   let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) ->
       let t = nf_evar t in
-      let uvars = Univ.LSet.union uvars (Univops.universes_of_constr t) in
+      let uvars = Univ.LSet.union uvars (Vars.universes_of_constr t) in
       uvars, (coe,t,imps))
       Univ.LSet.empty l
   in
@@ -173,7 +173,7 @@ let do_assumptions kind nl l =
       let t = replace_vars subst t in
       let refs, status' = declare_assumptions idl is_coe kind (t,uctx) ubinders imps nl in
       let subst' = List.map2
-          (fun {CAst.v=id} (c,u) -> (id, UnivGen.constr_of_global_univ (c,u)))
+          (fun {CAst.v=id} (c,u) -> (id, Constr.mkRef (c,u)))
           idl refs
       in
       subst'@subst, status' && status, next_uctx uctx)
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 5f340dc144..138696e3a7 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -266,7 +266,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
     let env = Global.env() in
     let indexes = search_guard env indexes fixdecls in
     let fiximps = List.map (fun (n,r,p) -> r) fiximps in
-    let vars = Univops.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
+    let vars = Vars.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
     let fixdecls =
       List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
     let evd = Evd.from_ctx ctx in
@@ -299,7 +299,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
     let fixdefs = List.map Option.get fixdefs in
     let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
     let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
-    let vars = Univops.universes_of_constr (List.hd fixdecls) in
+    let vars = Vars.universes_of_constr (List.hd fixdecls) in
     let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
     let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
     let evd = Evd.from_ctx ctx in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 5352cf5f8c..0ac97a74e4 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -487,8 +487,8 @@ let declare_definition prg =
   let typ = nf typ in
   let body = nf body in
   let uvars = Univ.LSet.union
-      (Univops.universes_of_constr typ)
-      (Univops.universes_of_constr body) in
+      (Vars.universes_of_constr typ)
+      (Vars.universes_of_constr body) in
   let uctx = UState.restrict prg.prg_ctx uvars in
   let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) uctx prg.prg_univdecl in
   let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in