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

Reviewed-by: ejgallego

4 files changed, 30 insertions, 2 deletions

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)
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.