{Univops -> Vars}.universes_of_constr

It's basically an occur check so it makes sense to put it in vars

11 files changed, 31 insertions, 37 deletions

diff --git a/engine/univops.ml b/engine/univops.ml
index 7f9672f828..c933641865 100644
--- a/engine/univops.ml
+++ b/engine/univops.ml
@@ -9,20 +9,8 @@
 (************************************************************************)
 
 open Univ
-open Constr
 
-let universes_of_constr c =
-  let rec aux s c =
-    match kind c with
-    | Const (c, u) ->
-          LSet.fold LSet.add (Instance.levels u) s
-    | Ind ((mind,_), u) | Construct (((mind,_),_), u) ->
-          LSet.fold LSet.add (Instance.levels u) s
-    | Sort u when not (Sorts.is_small u) ->
-      let u = Sorts.univ_of_sort u in
-      LSet.fold LSet.add (Universe.levels u) s
-    | _ -> Constr.fold aux s c
-  in aux LSet.empty c
+let universes_of_constr = Vars.universes_of_constr
 
 let restrict_universe_context (univs, csts) keep =
   let removed = LSet.diff univs keep in
diff --git a/engine/univops.mli b/engine/univops.mli
index 57a53597b9..0ed06bb204 100644
--- a/engine/univops.mli
+++ b/engine/univops.mli
@@ -13,6 +13,7 @@ open Univ
 
 (** Return the set of all universes appearing in [constr]. *)
 val universes_of_constr : constr -> LSet.t
+[@@ocaml.deprecated "Use [Vars.universes_of_constr]"]
 
 (** [restrict_universe_context (univs,csts) keep] restricts [univs] to
    the universes in [keep]. The constraints [csts] are adjusted so
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 7456ecea56..164a47dd9a 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -432,21 +432,8 @@ and execute_array env = Array.map (execute env)
 
 (* Derived functions *)
 
-let universe_levels_of_constr _env c =
-  let rec aux s c =
-    match kind c with
-    | Const (_c, u) ->
-       LSet.fold LSet.add (Instance.levels u) s
-    | Ind ((_mind,_), u) | Construct (((_mind,_),_), u) ->
-       LSet.fold LSet.add (Instance.levels u) s
-    | Sort u when not (Sorts.is_small u) ->
-      let u = Sorts.univ_of_sort u in
-      LSet.fold LSet.add (Universe.levels u) s
-    | _ -> Constr.fold aux s c
-  in aux LSet.empty c
-
 let check_wellformed_universes env c =
-  let univs = universe_levels_of_constr env c in
+  let univs = universes_of_constr c in
   try UGraph.check_declared_universes (universes env) univs
   with UGraph.UndeclaredLevel u ->
     error_undeclared_universe env u
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 9d5d79124b..7380a860dd 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -312,3 +312,17 @@ let subst_instance_constr subst c =
 let subst_instance_context s ctx = 
   if Univ.Instance.is_empty s then ctx
   else Context.Rel.map (fun x -> subst_instance_constr s x) ctx
+
+let universes_of_constr c =
+  let open Univ in
+  let rec aux s c =
+    match kind c with
+    | Const (_c, u) ->
+       LSet.fold LSet.add (Instance.levels u) s
+    | Ind ((_mind,_), u) | Construct (((_mind,_),_), u) ->
+       LSet.fold LSet.add (Instance.levels u) s
+    | Sort u when not (Sorts.is_small u) ->
+      let u = Sorts.univ_of_sort u in
+      LSet.fold LSet.add (Universe.levels u) s
+    | _ -> Constr.fold aux s c
+  in aux LSet.empty c
diff --git a/kernel/vars.mli b/kernel/vars.mli
index fdddbdb342..7c928e2694 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -139,3 +139,5 @@ val subst_univs_level_context : Univ.universe_level_subst -> Constr.rel_context
 (** Instance substitution for polymorphism. *)
 val subst_instance_constr : Instance.t -> constr -> constr
 val subst_instance_context : Instance.t -> Constr.rel_context -> Constr.rel_context
+
+val universes_of_constr : constr -> Univ.LSet.t
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 85e759d152..cf959bd11f 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -8,6 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+module CVars = Vars
 open Ltac_plugin
 open Pp
 open Util
@@ -150,7 +151,7 @@ let ic_unsafe c = (*FIXME remove *)
 
 let decl_constant na univs c =
   let open Constr in
-  let vars = Univops.universes_of_constr c in
+  let vars = CVars.universes_of_constr c in
   let univs = Univops.restrict_universe_context univs vars in
   let univs = Monomorphic_const_entry univs in
   mkConst(declare_constant (Id.of_string na) 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index de151fb6e5..25cf789193 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -347,8 +347,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
           not (Safe_typing.empty_private_constants = eff))
         in
         let typ = if allow_deferred then t else nf t in
-        let used_univs_body = Univops.universes_of_constr body in
-        let used_univs_typ = Univops.universes_of_constr typ in
+        let used_univs_body = Vars.universes_of_constr body in
+        let used_univs_typ = Vars.universes_of_constr typ in
         if allow_deferred then
           let initunivs = UState.const_univ_entry ~poly initial_euctx in
           let ctx = constrain_variables universes in
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 0ef5d56d4f..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
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