Commit 8eb17fc8 authored by Jan-Oliver Kaiser's avatar Jan-Oliver Kaiser
Browse files

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.
parent 6d64bcb5
Pipeline #66071 passed with stage
in 5 minutes and 35 seconds
...@@ -2,6 +2,11 @@ From stdpp Require Import tactics telescopes. ...@@ -2,6 +2,11 @@ From stdpp Require Import tactics telescopes.
Local Unset Mangle Names. (* for stable goal printing *) 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. Section accessor.
(* This is like Iris' accessors, but in Prop. Just to play with telescopes. *) (* This is like Iris' accessors, but in Prop. Just to play with telescopes. *)
Definition accessor {X : tele} (α β γ : X Prop) : Prop := Definition accessor {X : tele} (α β γ : X Prop) : Prop :=
...@@ -48,11 +53,6 @@ is essentially just a (dependent) product. ...@@ -48,11 +53,6 @@ is essentially just a (dependent) product.
*) *)
Definition no_bump@{u} (t : tele@{u}) : Type@{u} := tele_arg@{u} t. 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. (** [tele_arg ..] notation tests.
These tests mainly test type annotations and casts in the [tele_arg] These tests mainly test type annotations and casts in the [tele_arg]
notations. notations.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment