congruence: Restrict refreshing to Set

Because refreshing Prop is not semantics-preserving,
the new universe is >= Set, so cannot be minimized to Prop
afterwards.

2 files changed, 14 insertions, 21 deletions

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.