diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2018-06-05 12:00:40 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2018-06-05 12:00:40 +0200 |
| commit | 56be411d5c582d6f644129dabda7ba036a4419a7 (patch) | |
| tree | def26fef6fc8b864253040206a099b14c5823703 /engine/univops.mli | |
| parent | f6538f1a7f8ad2bdc0bc446d4ca35078d55d63ee (diff) | |
| parent | 3490e3c0b7bbd574228725f8132082c519d0f1a2 (diff) | |
Merge PR #7495: Fix restrict_universe_context
Diffstat (limited to 'engine/univops.mli')
| -rw-r--r-- | engine/univops.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/engine/univops.mli b/engine/univops.mli index d1585414c..0b37ab975 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 |