1 files changed, 20 insertions, 0 deletions
diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v
index a70d9196..bbfe5ec4 100644
--- a/test-suite/success/cc.v
+++ b/test-suite/success/cc.v
@@ -129,5 +129,25 @@ 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.
+
+(* Example by Jonathan Leivant, congruence up to universes *)
+Section JLeivant.
+  Variables S1 S2 : Set.
+
+  Definition T1 : Type := S1.
+  Definition T2 : Type := S2.
 
+  Goal T1 = T1.
+    congruence.
+    Undo.
+    unfold T1.
+    congruence.
+  Qed.
+End JLeivant.