From 44ecd58e9ab5fb0f2c45e9eec76440f84995825c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Oct 2018 14:20:51 +0200
Subject: {Univops -> Vars}.universes_of_constr

It's basically an occur check so it makes sense to put it in vars
---
 engine/univops.ml  | 14 +-------------
 engine/univops.mli |  1 +
 2 files changed, 2 insertions(+), 13 deletions(-)

(limited to 'engine')

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