From 04b9870f0ebe79fde789551c8e172aad1e7cfc5c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 08:52:01 +0100
Subject: Inherit argument scopes in notations to expressions of the form @f.

This is a change of semantics.
---
 interp/constrextern.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 362fe83ffa..7f5f03610b 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1211,8 +1211,7 @@ 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 =
-                if n = 0 then [] else try List.skipn n argsscopes with Failure _ -> [] in
+              let args2scopes = try List.skipn n argsscopes with Failure _ -> [] in
               let args2impls =
                 if n = 0 then
                   (* Note: NApp(NRef f,[]), hence n=0, encodes @f and
-- 
cgit v1.2.3