From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- engine/univops.mli | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'engine/univops.mli') diff --git a/engine/univops.mli b/engine/univops.mli index d1585414..57a53597 100644 --- a/engine/univops.mli +++ b/engine/univops.mli @@ -11,8 +11,11 @@ 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 -(** 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