From 71d4c435e42c24c21ae43f0ddcc7a71bee1009f5 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 9 May 2016 18:31:01 +0200
Subject: congruence: Restrict refreshing to Set

Because refreshing Prop is not semantics-preserving,
the new universe is >= Set, so cannot be minimized to Prop
afterwards.
---
 test-suite/success/cc.v         | 14 ++++++++++++++
 test-suite/success/congruence.v | 21 ---------------------
 2 files changed, 14 insertions(+), 21 deletions(-)
 delete mode 100644 test-suite/success/congruence.v

(limited to 'test-suite')

diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v
index a70d919635..0b0e93eb56 100644
--- a/test-suite/success/cc.v
+++ b/test-suite/success/cc.v
@@ -131,3 +131,17 @@ End bug_2447.
 
 
 
+(* 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.
diff --git a/test-suite/success/congruence.v b/test-suite/success/congruence.v
deleted file mode 100644
index 873d2f9f7e..0000000000
--- a/test-suite/success/congruence.v
+++ /dev/null
@@ -1,21 +0,0 @@
-(* Example by Jonathan Leivant, congruence and tauto up to universes *)
-Variables S1 S2 : Set.
-
-Goal @eq Type S1 S2 -> @eq Type S1 S2.
-intro H.
-tauto.
-Qed.
-
-Definition T1 : Type := S1.
-Definition T2 : Type := S2.
-
-Goal T1 = T1.
-congruence.
-Undo.
-tauto.
-Undo.
-unfold T1.
-congruence.
-Undo.
-tauto.
-Qed.
-- 
cgit v1.2.3