diff --git a/theories/telescopes.v b/theories/telescopes.v
index 1aaab4d1110e1b163dd4b0fb7b21aac2dc571aba..17b70cf6d075f4c706e2614408a5975af22e944b 100644
--- a/theories/telescopes.v
+++ b/theories/telescopes.v
@@ -1,6 +1,8 @@
 From stdpp Require Import base tactics.
 Set Default Proof Using "Type".
 
+Local Set Universe Polymorphism.
+
 (** Telescopes *)
 Inductive tele : Type :=
   | TeleO : tele