From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 test-suite/success/cc.v | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

(limited to 'test-suite/success/cc.v')

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.
-- 
cgit v1.2.3