diff options
| author | Gaëtan Gilbert | 2017-12-05 20:22:14 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-12-06 13:23:31 +0100 |
| commit | 5b8b02cd060097c3c980b0498257c30eda1ad207 (patch) | |
| tree | ff0e51230d3518bb2db523187644cd73d40aecf5 /API | |
| 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 'API')
| -rw-r--r-- | API/API.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/API/API.mli b/API/API.mli index 6227f17c65..b79be8f7dd 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2057,7 +2057,7 @@ end module Univops : sig - val universes_of_constr : Constr.constr -> Univ.LSet.t + val universes_of_constr : Environ.env -> Constr.constr -> Univ.LSet.t val restrict_universe_context : Univ.ContextSet.t -> Univ.LSet.t -> Univ.ContextSet.t end |