From d8dc892dc4e50462163053124c9bafcd312433a5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 5 Oct 2019 22:07:00 +0200
Subject: Notations: Avoiding computing parsing rule when in onlyprinting mode.

In particular, this fixes #9741.
---
 test-suite/bugs/closed/bug_9741.v | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_9741.v

(limited to 'test-suite/bugs')

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.
-- 
cgit v1.2.3