From 0acaa906367c02c57a6d70dd5d19eaea884b7568 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 10 May 2018 15:04:13 +0200
Subject: Fixes #7462, part 2 (only-printing not make believe parsing rule is
 declared).

---
 test-suite/bugs/closed/7462.v | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/7462.v b/test-suite/bugs/closed/7462.v
index 37af64caa2..40ca39e38a 100644
--- a/test-suite/bugs/closed/7462.v
+++ b/test-suite/bugs/closed/7462.v
@@ -4,3 +4,10 @@
 Notation "$ x" := (@id nat x) (only parsing, at level 0).
 Notation "$ x" := (@id bool x) (only printing, at level 0).
 Check $1. (* Was: Error: Unknown interpretation for notation "$ _". *)
+
+(* Adding an only-printing notation should not let believe
+   that a parsing rule has been given *)
+
+Notation "$ x" := (@id bool x) (only printing, at level 0).
+Notation "$ x" := (@id nat x) (only parsing, at level 0).
+Check $1. (* Was: Error: Syntax Error: Lexer: Undefined token *)
-- 
cgit v1.2.3