Merge PR #9214: Notations: Removing useless parentheses on abbreviations shortening a strict prefix of an application

Reviewed-by: ejgallego

2 files changed, 20 insertions, 0 deletions

diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 94016e170b..72d5a9253a 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -45,5 +45,9 @@ fun x : nat => (x.-1)%pred
      : Prop
 ##
      : Prop
+myAnd1 True True
+     : Prop
+r 2 3
+     : Prop
 Notation Cn := Foo.FooCn
 Expands to: Notation Top.J.Mfoo.Foo.Bar.Cn
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 309115848f..90babf9c55 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -165,6 +165,22 @@ Check ##.
 
 End H.
 
+(* Fixing bugs reported by G. Gonthier in #9207 *)
+
+Module I.
+
+Definition myAnd A B := A /\ B.
+Notation myAnd1 A := (myAnd A).
+Check myAnd1 True True.
+
+Set Warnings "-auto-template".
+
+Record Pnat := {inPnat :> nat -> Prop}.
+Axiom r : nat -> Pnat.
+Check r 2 3.
+
+End I.
+
 (* Fixing a bug reported by G. Gonthier in #9207 *)
 
 Module J.