diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-05 20:22:14 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-06 13:23:31 +0100 |
| commit | 5b8b02cd060097c3c980b0498257c30eda1ad207 (patch) | |
| tree | ff0e51230d3518bb2db523187644cd73d40aecf5 /engine/univops.mli | |
| parent | 2c5e81e3bc6ec17d253aeedd1b2bf4ccd3b81933 (diff) | |
Fix #6323: stronger restrict universe context vs abstract.
In the test we do [let X : Type@{i} := Set in ...] with Set
abstracted. The constraint [Set < i] was lost in the abstract.
Universes of a monomorphic reference [c] are considered to appear in
the term [c].
Diffstat (limited to 'engine/univops.mli')
| -rw-r--r-- | engine/univops.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/engine/univops.mli b/engine/univops.mli index 9af568bcb..30fcc4368 100644 --- a/engine/univops.mli +++ b/engine/univops.mli @@ -9,7 +9,8 @@ open Constr open Univ -(** Shrink a universe context to a restricted set of variables *) +(** The universes of monomorphic constants appear. *) +val universes_of_constr : Environ.env -> constr -> LSet.t -val universes_of_constr : constr -> LSet.t +(** Shrink a universe context to a restricted set of variables *) val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t |