Merge PR #13436: Fixes #13432: typo in #11172 causing notations mentioning a coercion not being used

Reviewed-by: ejgallego

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