From 134b220b77d74b0ada801d215a2e5c66bc6726ea Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 26 Nov 2017 19:18:38 +0100
Subject: Fixing associativity registered for level 10.

Apparently a long-standing bug, coupled with a pattern/constr
associativity inconsistency introduced while fixing another
pattern/constr level inconsistency (bug #4272, 0917ce7c).
---
 test-suite/success/Notations.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index e3f90f6d94..3c0ad20700 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -147,3 +147,9 @@ Inductive EQ {A} (x:A) : A -> Prop := REFL : x === x
 
 Fail Check {x@{u},y|x=x}.
 Fail Check {?[n],y|0=0}.
+
+(* Check that 10 is well declared left associative *)
+
+Section C.
+Notation "f $$$ x" := (id f x) (at level 10, left associativity).
+End C.
-- 
cgit v1.2.3