Deactivate implicit arguments in printing notations bound to "@f".

This is to match the parsing policy (see #11091).

In particular, we deactivate also argument scopes, consistently with
what is done at parsing time.

1 files changed, 8 insertions, 3 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 681d6ba541..362fe83ffa 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1211,9 +1211,14 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
         let (t,args,argsscopes,argsimpls) = match n with
           | Some n when nallargs >= n ->
               let args1, args2 = List.chop n args in
-              let args2scopes = try List.skipn n argsscopes with Failure _ -> [] in
-              let args2impls = try List.skipn n argsimpls with Failure _ -> [] in
-              (* Note: NApp(NRef f,[]), hence n=0, encodes @f *)
+              let args2scopes =
+                if n = 0 then [] else try List.skipn n argsscopes with Failure _ -> [] in
+              let args2impls =
+                if n = 0 then
+                  (* Note: NApp(NRef f,[]), hence n=0, encodes @f and
+                     conventionally deactivates implicit arguments *)
+                  []
+                else try List.skipn n argsimpls with Failure _ -> [] in
               DAst.make @@ GApp (f,args1), args2, args2scopes, args2impls
           | None ->
             begin match DAst.get f with