From 556e9dde62b6822db20bd5c7e6e6a67bc717c408 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 07:31:37 +0100
Subject: 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.
---
 interp/constrextern.ml | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

(limited to 'interp')

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
-- 
cgit v1.2.3