From 5dd690ee5975262d34d8dcc44191138c8d326f65 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 16 Jul 2016 16:24:59 +0200
Subject: Fixing a collision about the meta-variable ".." in recursive
 notations.

This happens when recursive notations are used to define recursive
notations.
---
 test-suite/success/Notations.v | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index b72a067407..2f7c62972a 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -107,3 +107,6 @@ Notation traverse_var f l := (traverse (fun l => f l) l).
 
 Notation "'intros' x" := (S x) (at level 0).
 Goal True -> True. intros H. exact H. Qed.
+
+(* Check absence of collision on ".." in nested notations with ".." *)
+Notation "[ a , .. , b ]" := (a, (.. (b,tt) ..)).
-- 
cgit v1.2.3