diff --git a/theories/telescopes.v b/theories/telescopes.v
index 7209cb9d06035940c060ce35b269ceaead744ee5..b78eff49538e9cf773571d472c8a1dc8b28f9273 100644
--- a/theories/telescopes.v
+++ b/theories/telescopes.v
@@ -143,7 +143,7 @@ Notation "'[tele_arg' ]" := (TargO)
 Notation "'λ..' x .. y , e" :=
   (tele_app (tele_bind (λ x, .. (tele_app (tele_bind (λ y, e))) .. )))
   (at level 200, x binder, y binder, right associativity,
-   format "'[  ' 'λ..'  x  ..  y ']' ,  e").
+   format "'[  ' 'λ..'  x  ..  y ']' ,  e") : stdpp_scope.
 
 (** Telescopic quantifiers *)
 Definition tforall {TT : tele} (Ψ : TT → Prop) : Prop :=