From 33d86118c7d1bfba31008b410d81c7f45dbdf092 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 29 Jul 2018 02:39:32 +0200
Subject: A test on the different ways to indicate the levels of a rule.

This is in preparation of changes in level_eq, to check that the
semantics is preserved.
---
 test-suite/success/Notations2.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index 7c2cf3ee52..d01ebfb18e 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -126,3 +126,11 @@ Notation "'myexists' x , p" := (ex (fun x => p))
   (at level 200, x ident, p at level 200, right associativity) : type_scope.
 Check myexists I, I = 0. (* Should not be seen as a constructor *)
 End M14.
+
+(* 15. Testing different ways to give the same levels without failing *)
+
+Module M15.
+  Local Notation "###### x" := (S x) (right associativity, at level 79, x at next level).
+  Fail Local Notation "###### x" := (S x) (right associativity, at level 79).
+  Local Notation "###### x" := (S x) (at level 79).
+End M15.
-- 
cgit v1.2.3