diff options
Diffstat (limited to 'test-suite/success/cc.v')
| -rw-r--r-- | test-suite/success/cc.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v index a70d91963..dc0527d82 100644 --- a/test-suite/success/cc.v +++ b/test-suite/success/cc.v @@ -129,5 +129,10 @@ Qed. End bug_2447. +(* congruence was supposed to do discriminate but it was bugged for + types with indices *) - +Inductive I : nat -> Type := C : I 0 | D : I 0. +Goal ~C=D. +congruence. +Qed. |