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.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/eConstr.mli')

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