From 5325f9f0d986e0fbf2332bacd880295db927b8cf Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 24 Jan 2019 19:16:46 +0100
Subject: [PATCH] put notation into stdpp_scope

---
 theories/telescopes.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/telescopes.v b/theories/telescopes.v
index 7209cb9d..b78eff49 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 :=
-- 
GitLab