From 41d60ea7bf034a92e2fabee40ad435ba8363a2d6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 12 Dec 2018 18:56:29 +0100
Subject: Notations: Removing useless parentheses on abbrevs for prefix of an
 application.

---
 interp/constrextern.ml           |  9 +++++++--
 test-suite/output/Notations4.out |  4 ++++
 test-suite/output/Notations4.v   | 16 ++++++++++++++++
 3 files changed, 27 insertions(+), 2 deletions(-)

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 444ac5ab6d..13078840ef 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -625,8 +625,13 @@ let explicitize inctx impl (cf,f) args =
 	  CApp ((ip,f),args1@args2)
     | None ->
       let args = exprec 1 (args,impl) in
-	if List.is_empty args then f.CAst.v else CApp ((None, f), args)
-  in
+        if List.is_empty args then f.CAst.v else
+          match f.CAst.v with
+          | CApp (g,args') ->
+              (* may happen with notations for a prefix of an n-ary
+                 application *)
+              CApp (g,args'@args)
+          | _ -> CApp ((None, f), args) in
     try expl ()
     with Expl -> 
       let f',us = match f with { CAst.v = CRef (f,us) } -> f,us | _ -> assert false in
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.
-- 
cgit v1.2.3


From 25014277624387ecba1befb60f1c54d68eadab01 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 25 Jan 2019 10:30:53 +0100
Subject: Added a line about notation bug fixes.

---
 CHANGES.md | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/CHANGES.md b/CHANGES.md
index bcdb951a94..4b0cf31a1f 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -49,6 +49,9 @@ Notations
 - New command `String Notation` to register string syntax for custom
   inductive types.
 
+- Various bugs have been fixed (e.g. PR #9214 on removing spurious
+  parentheses on abbreviations shortening a strict prefix of an application).
+
 Plugins
 
 - The quote plugin (https://coq.inria.fr/distrib/V8.8.1/refman/proof-engine/detailed-tactic-examples.html#quote)
-- 
cgit v1.2.3