From 05dff3bdaaf474e67b0878bc2dd0952427ce277e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Fri, 22 Jun 2018 16:09:23 +0200
Subject: universes_of_constr don't include universes of monomorphic constants

Apparently it was not useful. I don't remember what I was thinking
when I added it.
---
 engine/eConstr.ml  | 13 +------------
 engine/eConstr.mli |  2 +-
 engine/univops.ml  | 15 ++-------------
 engine/univops.mli |  4 ++--
 4 files changed, 6 insertions(+), 28 deletions(-)

(limited to 'engine')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 6810626ad..005ef1635 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -592,25 +592,14 @@ let eq_constr_universes_proj env sigma m n =
     let res = eq_constr' 0 (unsafe_to_constr m) (unsafe_to_constr n) in
     if res then Some !cstrs else None
 
-let universes_of_constr env sigma c =
+let universes_of_constr 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
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index e9d3e782b..913825a9f 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -232,7 +232,7 @@ val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a
 
 (** Gather the universes transitively used in the term, including in the
    type of evars appearing in it. *)
-val universes_of_constr : Environ.env -> Evd.evar_map -> t -> Univ.LSet.t
+val universes_of_constr : Evd.evar_map -> t -> Univ.LSet.t
 
 (** {6 Substitutions} *)
 
diff --git a/engine/univops.ml b/engine/univops.ml
index 3fd518490..7f9672f82 100644
--- a/engine/univops.ml
+++ b/engine/univops.ml
@@ -11,24 +11,13 @@
 open Univ
 open Constr
 
-let universes_of_constr env c =
-  let open Declarations in
-  let rec aux s c = 
+let universes_of_constr c =
+  let rec aux s c =
     match kind c with
     | Const (c, u) ->
-      begin match (Environ.lookup_constant c env).const_universes with
-        | Polymorphic_const _ ->
           LSet.fold LSet.add (Instance.levels 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 u) s
-        | Monomorphic_ind (univs,_) ->
-          LSet.union s univs
-      end
     | Sort u when not (Sorts.is_small u) ->
       let u = Sorts.univ_of_sort u in
       LSet.fold LSet.add (Universe.levels u) s
diff --git a/engine/univops.mli b/engine/univops.mli
index 0b37ab975..57a53597b 100644
--- a/engine/univops.mli
+++ b/engine/univops.mli
@@ -11,8 +11,8 @@
 open Constr
 open Univ
 
-(** The universes of monomorphic constants appear. *)
-val universes_of_constr : Environ.env -> constr -> LSet.t
+(** Return the set of all universes appearing in [constr]. *)
+val universes_of_constr : constr -> LSet.t
 
 (** [restrict_universe_context (univs,csts) keep] restricts [univs] to
    the universes in [keep]. The constraints [csts] are adjusted so
-- 
cgit v1.2.3