From 835d3d76b33d9d7761a1ba189003db36c253ce28 Mon Sep 17 00:00:00 2001
From: Gregory Malecha <gmalecha@gmail.com>
Date: Thu, 7 Apr 2022 01:55:49 +0000
Subject: [PATCH] Use unicode and fix comment.

---
 tests/telescopes.v    | 5 +++--
 theories/telescopes.v | 7 ++++---
 2 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/tests/telescopes.v b/tests/telescopes.v
index fb7295f7..e282b131 100644
--- a/tests/telescopes.v
+++ b/tests/telescopes.v
@@ -48,6 +48,7 @@ is essentially just a (dependent) product.
  *)
 Definition no_bump@{u} (t : tele@{u}) : Type@{u} := tele_arg@{u} t.
 
-Lemma texist_exist_universes (X : Type) (P : TeleS (fun _ : X => TeleO) -> Prop) :
-  texist P <-> ex P.
+(** 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.
diff --git a/theories/telescopes.v b/theories/telescopes.v
index 028d444f..b44ecc82 100644
--- a/theories/telescopes.v
+++ b/theories/telescopes.v
@@ -3,8 +3,9 @@ From stdpp Require Import options.
 
 Local Set Universe Polymorphism.
 
-(* Without this flag, Coq minimizes some universes to [Set] when they
-   should not be, e.g. in [texist_exist]. *)
+(** Without this flag, Coq minimizes some universes to [Set] when they
+    should not be, e.g. in [texist_exist].
+    See the [texist_exist_universes] test. *)
 Local Unset Universe Minimization ToSet.
 
 (** Telescopes *)
@@ -75,7 +76,7 @@ Lemma tele_arg_inv {TT : tele} (a : tele_arg TT) :
   | TeleS f => λ a, ∃ x a', a = TargS x a'
   end a.
 Proof. destruct TT; destruct a; eauto. Qed.
-Lemma tele_arg_O_inv (a : TeleO) : a = ().
+Lemma tele_arg_O_inv (a : TeleO) : a = TargO.
 Proof. exact (tele_arg_inv a). Qed.
 Lemma tele_arg_S_inv {X} {f : X → tele} (a : TeleS f) :
   ∃ x a', a = TargS x a'.
-- 
GitLab