diff options
| author | Matthieu Sozeau | 2016-07-05 18:28:24 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-07-05 18:29:37 +0200 |
| commit | 57021d22fabb33b281af4de8f3946cb4424c6422 (patch) | |
| tree | 031746971a3bf3118b7473426791f32d5aa079a9 | |
| parent | 37293bd104434bb15acc7d46b8cba90e70504aac (diff) | |
congruence fix: test-suite code and update CHANGES
This fixes bugs #4069 (not 4609 as mentionned in the git log) and #4718.
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4069.v | 16 |
2 files changed, 16 insertions, 1 deletions
@@ -24,6 +24,7 @@ Other bugfixes - #4882: anomaly with Declare Implicit Tactic on hole of type with evars - Fix use of "Declare Implicit Tactic" in refine. triggered by CoqIDE +- #4069, #4718: congruence fails when universes are involved. Universes - Disallow silently dropping universe instances applied to variables diff --git a/test-suite/bugs/closed/4069.v b/test-suite/bugs/closed/4069.v index 11289f7575..61527764e2 100644 --- a/test-suite/bugs/closed/4069.v +++ b/test-suite/bugs/closed/4069.v @@ -87,4 +87,18 @@ f_equal. Undo 2. unshelve refine (tequator (X _)); revgoals. f_equal. -Admitted.
\ No newline at end of file +Admitted. + +Goal @eq Set nat nat. +congruence. +Qed. + +Goal @eq Type nat nat. +congruence. +Qed. + +Variable T : Type. + +Goal @eq Type T T. +congruence. +Qed.
\ No newline at end of file |