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.

1 files changed, 8 insertions, 6 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  *)