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 /test-suite/success | |
| 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 'test-suite/success')
| -rw-r--r-- | test-suite/success/congruence.v | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/test-suite/success/congruence.v b/test-suite/success/congruence.v new file mode 100644 index 0000000000..873d2f9f7e --- /dev/null +++ b/test-suite/success/congruence.v @@ -0,0 +1,21 @@ +(* Example by Jonathan Leivant, congruence and tauto up to universes *) +Variables S1 S2 : Set. + +Goal @eq Type S1 S2 -> @eq Type S1 S2. +intro H. +tauto. +Qed. + +Definition T1 : Type := S1. +Definition T2 : Type := S2. + +Goal T1 = T1. +congruence. +Undo. +tauto. +Undo. +unfold T1. +congruence. +Undo. +tauto. +Qed. |