Fixes #13432: regression with notations involving coercions caused by #11172.

In #11172, an "=" on the number of arguments of an applied coercion
had become a ">" on the number of arguments of the coercion. It should
have been a ">=". The rest of changes in constrextern.ml is "cosmetic".

Note that in #11172, in the case of a coercion to funclass, the
definition of number of arguments of an applied coercion had moved
from including the extra arguments of the coercion to funclass to
exactly the nomber of arguments of the coercion (excluding the extra
arguments). This was necessary to take into account that several
coercions can be nested, at least of those involving a coercion to
funclass.

Incidentally, we create a dedicated output file for notations and
coercions.

5 files changed, 115 insertions, 64 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index cf88036f73..378adb566c 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -800,19 +800,21 @@ let extern_args extern env args =
 let match_coercion_app c = match DAst.get c with
   | GApp (r, args) ->
     begin match DAst.get r with
-    | GRef (r,_) -> Some (c.CAst.loc, r, 0, args)
+    | GRef (r,_) -> Some (c.CAst.loc, r, args)
     | _ -> None
     end
   | _ -> None
 
 let remove_one_coercion inctx c =
   try match match_coercion_app c with
-  | Some (loc,r,pars,args) when not (!Flags.raw_print || !print_coercions) ->
+  | Some (loc,r,args) when not (!Flags.raw_print || !print_coercions) ->
       let nargs = List.length args in
       (match Coercionops.hide_coercion r with
-          | Some n when (n - pars) < nargs && (inctx || (n - pars)+1 < nargs) ->
+          | Some nparams when
+                 let inctx = inctx || (* coercion to funclass implying being in context *) nparams+1 < nargs in
+                 nparams < nargs && inctx ->
               (* We skip the coercion *)
-              let l = List.skipn (n - pars) args in
+              let l = List.skipn nparams args in
               let (a,l) = match l with a::l -> (a,l) | [] -> assert false in
               (* Don't flatten App's in case of funclass so that
                  (atomic) notations on [a] work; should be compatible
@@ -824,7 +826,7 @@ let remove_one_coercion inctx c =
                  have been made explicit to match *)
               let a' = if List.is_empty l then a else DAst.make ?loc @@ GApp (a,l) in
               let inctx = inctx || not (List.is_empty l) in
-              Some (n-pars+1, inctx, a')
+              Some (nparams+1, inctx, a')
           | _ -> None)
   | _ -> None
   with Not_found ->
@@ -867,7 +869,7 @@ let filter_enough_applied nargs l =
   | Some nargs ->
   List.filter (fun (keyrule,pat,n as _rule) ->
       match n with
-      | AppBoundedNotation n -> n > nargs
+      | AppBoundedNotation n -> n >= nargs
       | AppUnboundedNotation | NotAppNotation -> false) l
 
 (* Helper function for safe and optimal printing of primitive tokens  *)
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index df64ae2af3..3477a293e3 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -31,12 +31,6 @@ end
      : Expr -> Expr
 [(1 + 1)]
      : Expr
-Let "x" e1 e2
-     : expr
-Let "x" e1 e2
-     : expr
-Let "x" e1 e2 : list string
-     : list string
 myAnd1 True True
      : Prop
 r 2 3
@@ -65,8 +59,6 @@ where
       |- Type] (pat, p0, p cannot be used)
 fun '{| |} => true
      : R -> bool
-b = a
-     : Prop
 The command has indeed failed with message:
 The format is not the same on the right- and left-hand sides of the special token "..".
 The command has indeed failed with message:
@@ -85,18 +77,18 @@ fun x : nat => [x]
      : nat -> nat
 ∀ x : nat, x = x
      : Prop
-File "stdin", line 226, characters 0-160:
+File "stdin", line 184, characters 0-160:
 Warning: Notation "∀ _ .. _ , _" was already defined with a different format
 in scope type_scope. [notation-incompatible-format,parsing]
 ∀x : nat,x = x
      : Prop
-File "stdin", line 239, characters 0-60:
+File "stdin", line 197, characters 0-60:
 Warning: Notation "_ %%% _" was already defined with a different format.
 [notation-incompatible-format,parsing]
-File "stdin", line 243, characters 0-64:
+File "stdin", line 201, characters 0-64:
 Warning: Notation "_ %%% _" was already defined with a different format.
 [notation-incompatible-format,parsing]
-File "stdin", line 248, characters 0-62:
+File "stdin", line 206, characters 0-62:
 Warning: Lonely notation "_ %%%% _" was already defined with a different
 format. [notation-incompatible-format,parsing]
 3  %%  4
@@ -105,10 +97,10 @@ format. [notation-incompatible-format,parsing]
      : nat
 3   %%   4
      : nat
-File "stdin", line 276, characters 0-61:
+File "stdin", line 234, characters 0-61:
 Warning: The format modifier is irrelevant for only parsing rules.
 [irrelevant-format-only-parsing,parsing]
-File "stdin", line 280, characters 0-63:
+File "stdin", line 238, characters 0-63:
 Warning: The only parsing modifier has no effect in Reserved Notation.
 [irrelevant-reserved-notation-only-parsing,parsing]
 fun x : nat => U (S x)
@@ -119,7 +111,7 @@ fun x : nat => V x
      : forall x : nat, nat * (?T -> ?T)
 where
 ?T : [x : nat  x0 : ?T |- Type] (x0 cannot be used)
-File "stdin", line 297, characters 0-30:
+File "stdin", line 255, characters 0-30:
 Warning: Notation "_ :=: _" was already used. [notation-overridden,parsing]
 0 :=: 0
      : Prop
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index ebc1426fc8..eaff50beb7 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -79,35 +79,7 @@ Check [1 + 1].
 
 End C.
 
-(* An example of interaction between coercion and notations from
-   Robbert Krebbers. *)
-
-Require Import String.
-
-Module D.
-
-Inductive expr :=
-  | Var : string -> expr
-  | Lam : string -> expr -> expr
-  | App : expr -> expr -> expr.
-
-Notation Let x e1 e2 := (App (Lam x e2) e1).
-
-Parameter e1 e2 : expr.
-
-Check (Let "x" e1 e2).
-
-Coercion App : expr >-> Funclass.
-
-Check (Let "x" e1 e2).
-
-Axiom free_vars :> expr -> list string.
-
-Check (Let "x" e1 e2) : list string.
-
-End D.
-
-(* Fixing bugs reported by G. Gonthier in #9207 *)
+(* Fixing overparenthesizing reported by G. Gonthier in #9207 (PR #9214, in 8.10)*)
 
 Module I.
 
@@ -152,20 +124,6 @@ Check fun '{|n:=x|} => true.
 
 End EmptyRecordSyntax.
 
-Module L.
-
-(* Testing regression #11053 *)
-
-Section Test.
-Variables (A B : Type) (a : A) (b : B).
-Variable c : A -> B.
-Coercion c : A >-> B.
-Notation COERCION := (c).
-Check b = a.
-End Test.
-
-End L.
-
 Module M.
 
 (* Accept boxes around the end variables of a recursive notation (if equal boxes) *)
diff --git a/test-suite/output/NotationsCoercions.out b/test-suite/output/NotationsCoercions.out
new file mode 100644
index 0000000000..56145e5fa5
--- /dev/null
+++ b/test-suite/output/NotationsCoercions.out
@@ -0,0 +1,22 @@
+Let "x" e1 e2
+     : expr
+Let "x" e1 e2
+     : expr
+Let "x" e1 e2 : list string
+     : list string
+b = a
+     : Prop
+foo
+     : (_ BitVec 32)
+#[ r ] 0
+     : nat
+##[ r ]
+     : nat
+##[ r ]
+     : nat
+#[ r ] 0
+     : nat
+##[ r ]
+     : nat
+##[ r ]
+     : nat
diff --git a/test-suite/output/NotationsCoercions.v b/test-suite/output/NotationsCoercions.v
new file mode 100644
index 0000000000..0524bed98c
--- /dev/null
+++ b/test-suite/output/NotationsCoercions.v
@@ -0,0 +1,77 @@
+(* Tests about skipping a coercion vs using a notation involving a coercion *)
+
+Require Import String.
+
+(* Skipping a coercion vs using a notation for the application of the
+    coercion (from Robbert Krebbers, see PR #8890) *)
+
+Module A.
+
+Inductive expr :=
+  | Var : string -> expr
+  | Lam : string -> expr -> expr
+  | App : expr -> expr -> expr.
+
+Notation Let x e1 e2 := (App (Lam x e2) e1).
+Parameter e1 e2 : expr.
+Check (Let "x" e1 e2). (* always printed the same *)
+Coercion App : expr >-> Funclass.
+Check (Let "x" e1 e2). (* printed the same from #8890, in 8.10 *)
+Axiom free_vars :> expr -> list string.
+Check (Let "x" e1 e2) : list string. (* printed the same from #11172, in 8.12 *)
+
+End A.
+
+(* Skipping a coercion vs using a notation for the coercion itself
+   (regression #11053 in 8.10 after PR #8890, addressed by PR #11090) *)
+
+Module B.
+
+Section Test.
+Variables (A B : Type) (a : A) (b : B).
+Variable c : A -> B.
+Coercion c : A >-> B.
+Notation COERCION := (c).
+Check b = a. (* printed the same except in 8.10 *)
+End Test.
+
+End B.
+
+Module C.
+
+Record word := { rep: Type }.
+Coercion rep : word >-> Sortclass.
+Axiom myword: word.
+Axiom foo: myword.
+Notation "'(_' 'BitVec' '32)'" := (rep myword).
+Check foo. (* printed with Bitvec from #8890 in 8.10 and 8.11, regression due to #11172 in 8.12 *)
+
+End C.
+
+(* Examples involving coercions to funclass *)
+
+Module D.
+
+Record R := { f :> nat -> nat }.
+Axiom r : R.
+Notation "#[ x  ]" := (f x).
+Check #[ r ] 0. (* printed the same from 8.10 (due to #8890), but not 8.11 and 8.12 (due to #11090) *)
+Notation "##[ x  ]" := (f x 0).
+Check ##[ r ]. (* printed the same from 8.10 *)
+Check #[ r ] 0. (* printed ##[ r ] from 8.10 *)
+
+End D.
+
+(* Same examples with a parameter *)
+
+Module E.
+
+Record R A := { f :> A -> A }.
+Axiom r : R nat.
+Notation "#[ x  ]" := (f nat x).
+Check #[ r ] 0. (* printed the same from 8.10 (due to #8890), but not 8.11 and 8.12 (due to #11090) *)
+Notation "##[ x  ]" := (f nat x 0).
+Check ##[ r ]. (* printed the same from 8.10 *)
+Check #[ r ] 0. (* printed ##[ r ] from 8.10 *)
+
+End E.