Merge PR #11590: Fixes #9741: only printing notations do not uselessly reserve parsing keywords

Reviewed-by: ejgallego

1 files changed, 21 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_9741.v b/test-suite/bugs/closed/bug_9741.v
new file mode 100644
index 0000000000..247155d8b3
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9741.v
@@ -0,0 +1,21 @@
+(* This was failing at parsing *)
+
+Notation "'a'" := tt (only printing).
+Goal True. let a := constr:(1+1) in idtac a. Abort.
+
+(* Idem *)
+
+Require Import Coq.Strings.String.
+Require Import Coq.ZArith.ZArith.
+Open Scope string_scope.
+
+Axiom Ox: string -> Z.
+
+Axiom isMMIOAddr: Z -> Prop.
+
+Notation "'Ox' a" := (Ox a) (only printing, at level 10, format "'Ox' a").
+
+Goal False.
+  set (f := isMMIOAddr).
+  set (x := f (Ox "0018")).
+Abort.