From a52a2d2110fcf20d532a2005c1957cba0d2c4043 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 11 May 2018 14:43:44 +0200
Subject: Fix restrict_universe_context

---
 engine/univops.mli | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'engine/univops.mli')

diff --git a/engine/univops.mli b/engine/univops.mli
index d1585414c1..0b37ab975d 100644
--- a/engine/univops.mli
+++ b/engine/univops.mli
@@ -14,5 +14,8 @@ open Univ
 (** The universes of monomorphic constants appear. *)
 val universes_of_constr : Environ.env -> constr -> LSet.t
 
-(** Shrink a universe context to a restricted set of variables *)
+(** [restrict_universe_context (univs,csts) keep] restricts [univs] to
+   the universes in [keep]. The constraints [csts] are adjusted so
+   that transitive constraints between remaining universes (those in
+   [keep] and those not in [univs]) are preserved. *)
 val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t
-- 
cgit v1.2.3