1 files changed, 15 insertions, 0 deletions
diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v
index dc0527d82..bbfe5ec42 100644
--- a/test-suite/success/cc.v
+++ b/test-suite/success/cc.v
@@ -136,3 +136,18 @@ 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.