From 93d78065b639f9e77c9ccfa791eb8f3bbb8e0b37 Mon Sep 17 00:00:00 2001
From: Gregory Malecha <gregory@bedrocksystems.com>
Date: Mon, 7 Mar 2022 23:39:20 -0500
Subject: [PATCH] Document the need for [Unset Universe Minimization ToSet].

---
 theories/telescopes.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/theories/telescopes.v b/theories/telescopes.v
index a66c5c50..b7410fb2 100644
--- a/theories/telescopes.v
+++ b/theories/telescopes.v
@@ -2,6 +2,9 @@ From stdpp Require Import base tactics.
 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]. *)
 Local Unset Universe Minimization ToSet.
 
 (** Telescopes *)
-- 
GitLab