From 57021d22fabb33b281af4de8f3946cb4424c6422 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 5 Jul 2016 18:28:24 +0200
Subject: congruence fix: test-suite code and update CHANGES

This fixes bugs #4069 (not 4609 as mentionned in the git log) and #4718.
---
 CHANGES                       |  1 +
 test-suite/bugs/closed/4069.v | 16 +++++++++++++++-
 2 files changed, 16 insertions(+), 1 deletion(-)

diff --git a/CHANGES b/CHANGES
index 0f5ea97aa2..7d5691efe7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -24,6 +24,7 @@ Other bugfixes
 - #4882: anomaly with Declare Implicit Tactic on hole of type with evars
 - Fix use of "Declare Implicit Tactic" in refine.
   triggered by CoqIDE
+- #4069, #4718: congruence fails when universes are involved.
 
 Universes
 - Disallow silently dropping universe instances applied to variables
diff --git a/test-suite/bugs/closed/4069.v b/test-suite/bugs/closed/4069.v
index 11289f7575..61527764e2 100644
--- a/test-suite/bugs/closed/4069.v
+++ b/test-suite/bugs/closed/4069.v
@@ -87,4 +87,18 @@ f_equal.
 Undo 2.
 unshelve refine (tequator (X _)); revgoals.
 f_equal.
-Admitted.
\ No newline at end of file
+Admitted.
+
+Goal @eq Set nat nat.
+congruence.
+Qed.
+
+Goal @eq Type nat nat.
+congruence. 
+Qed.
+
+Variable T : Type.
+
+Goal @eq Type T T.
+congruence.
+Qed.
\ No newline at end of file
-- 
cgit v1.2.3