diff --git a/theories/telescopes.v b/theories/telescopes.v
index a66c5c506d27e80491c13df5a32df836258749a5..b7410fb218cb2205c7d8d94031e22aa74fe7d3d4 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 *)