1 files changed, 37 insertions, 7 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index bcfbc8081e..d303038c5d 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -9,7 +9,6 @@
 open CErrors
 open Util
 open Names
-open Term
 open Constr
 open Context
 open Evd
@@ -55,7 +54,7 @@ struct
   type t = Sorts.t
   let make s = s
   let kind sigma = function
-  | Type u -> sort_of_univ (Evd.normalize_universe sigma u)
+  | Sorts.Type u -> Sorts.sort_of_univ (Evd.normalize_universe sigma u)
   | s -> s
   let unsafe_to_sorts s = s
 end
@@ -85,16 +84,16 @@ let rec whd_evar sigma c =
     | Some c -> whd_evar sigma c
     | None -> c
     end
-  | App (f, args) when Term.isEvar f ->
+  | App (f, args) when isEvar f ->
     (** Enforce smart constructor invariant on applications *)
-    let ev = Term.destEvar f in
+    let ev = destEvar f in
     begin match safe_evar_value sigma ev with
     | None -> c
     | Some f -> whd_evar sigma (mkApp (f, args))
     end
-  | Cast (c0, k, t) when Term.isEvar c0 ->
+  | Cast (c0, k, t) when isEvar c0 ->
     (** Enforce smart constructor invariant on casts. *)
-    let ev = Term.destEvar c0 in
+    let ev = destEvar c0 in
     begin match safe_evar_value sigma ev with
     | None -> c
     | Some c -> whd_evar sigma (mkCast (c, k, t))
@@ -115,7 +114,7 @@ let rec to_constr sigma c = match Constr.kind c with
   | Some c -> to_constr sigma c
   | None -> Constr.map (fun c -> to_constr sigma c) c
   end
-| Sort (Type u) ->
+| Sort (Sorts.Type u) ->
   let u' = Evd.normalize_universe sigma u in
   if u' == u then c else mkSort (Sorts.sort_of_univ u')
 | Const (c', u) when not (Univ.Instance.is_empty u) ->
@@ -646,6 +645,37 @@ let eq_constr_universes_proj env sigma m n =
     let res = eq_constr' (unsafe_to_constr m) (unsafe_to_constr n) in
     if res then Some !cstrs else None
 
+let universes_of_constr env sigma c =
+  let open Univ in
+  let open Declarations in
+  let rec aux s c =
+    match kind sigma c with
+    | Const (c, u) ->
+      begin match (Environ.lookup_constant c env).const_universes with
+        | Polymorphic_const _ ->
+          LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
+        | Monomorphic_const (univs, _) ->
+          LSet.union s univs
+      end
+    | Ind ((mind,_), u) | Construct (((mind,_),_), u) ->
+      begin match (Environ.lookup_mind mind env).mind_universes with
+        | Cumulative_ind _ | Polymorphic_ind _ ->
+          LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
+        | Monomorphic_ind (univs,_) ->
+          LSet.union s univs
+      end
+    | Sort u ->
+       let sort = ESorts.kind sigma u in
+       if Sorts.is_small sort then s
+       else
+         let u = Sorts.univ_of_sort sort in
+         LSet.fold LSet.add (Universe.levels u) s
+    | Evar (k, args) ->
+       let concl = Evd.evar_concl (Evd.find sigma k) in
+       fold sigma aux (aux s (of_constr concl)) c
+    | _ -> fold sigma aux s c
+  in aux LSet.empty c
+
 open Context
 open Environ