From eb0feed6d22c11c44e7091c64ce5b1c9d5af987a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 5 Mar 2016 18:23:05 +0100
Subject: Using build_selector from Equality as a replacement of the selector
 in cctac which does not support indices properly.

Incidentally, this should fix a failure in RelationAlgebra, where
making prod_applist more robust (e8c47b652) revealed the discriminate
bug in congruence.
---
 test-suite/success/cc.v | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v
index a70d919635..dc0527d826 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.
-- 
cgit v1.2.3