From 8eb17fc82e690cd44e1a1f5b29f086b4cbd8504a Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@bedrocksystems.com>
Date: Mon, 16 May 2022 14:18:41 +0200
Subject: [PATCH] Move `Universe Minimization ToSet` test case higher.

The accessor test case also fails when the flag is enabled so that
the dedicated test case for it never has a chance to run.
---
 tests/telescopes.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/tests/telescopes.v b/tests/telescopes.v
index 416d29c8..30027fb5 100644
--- a/tests/telescopes.v
+++ b/tests/telescopes.v
@@ -2,6 +2,11 @@ From stdpp Require Import tactics telescopes.
 
 Local Unset Mangle Names. (* for stable goal printing *)
 
+(** This test would fail without [Unset Universe Minimization ToSet] in [telescopes.v]. *)
+Lemma texist_exist_universes (X : Type) (P : TeleS (λ _ : X, TeleO) → Prop) :
+  texist P ↔ ex P.
+Proof. by rewrite texist_exist. Qed.
+
 Section accessor.
 (* This is like Iris' accessors, but in Prop.  Just to play with telescopes. *)
 Definition accessor {X : tele} (α β γ : X → Prop) : Prop :=
@@ -48,11 +53,6 @@ is essentially just a (dependent) product.
  *)
 Definition no_bump@{u} (t : tele@{u}) : Type@{u} := tele_arg@{u} t.
 
-(** This test would fail without [Unset Universe Minimization ToSet] in [telescopes.v]. *)
-Lemma texist_exist_universes (X : Type) (P : TeleS (λ _ : X, TeleO) → Prop) :
-  texist P ↔ ex P.
-Proof. by rewrite texist_exist. Qed.
-
 (** [tele_arg ..] notation tests.
     These tests mainly test type annotations and casts in the [tele_arg]
     notations.
-- 
GitLab