diff options
| author | Matthieu Sozeau | 2016-05-09 17:40:04 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-07-04 15:48:15 +0200 |
| commit | a5b631f7260e7d29defd8bd5c67db543742c9ecd (patch) | |
| tree | ae3ccf9bcc9d46319abc3694415629487dd089c7 /kernel | |
| parent | 2ce64cc3124d30dbd42324c345cec378ccd66106 (diff) | |
congruence/univs: properly refresh (fix #4609)
In congruence, refresh universes including the Set/Prop ones so that
congruence works with cumulativity, not restricting itself to the
inferred types of terms that are manipulated but allowing them to be
used at more general types. This fixes bug #4609.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions