diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-07-05 18:28:24 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-07-05 18:29:37 +0200 |
| commit | 57021d22fabb33b281af4de8f3946cb4424c6422 (patch) | |
| tree | 031746971a3bf3118b7473426791f32d5aa079a9 /test-suite/bugs/closed/4069.v | |
| 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.
Diffstat (limited to 'test-suite/bugs/closed/4069.v')
| -rw-r--r-- | test-suite/bugs/closed/4069.v | 16 |
1 files changed, 15 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/4069.v b/test-suite/bugs/closed/4069.v index 11289f757..61527764e 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 |