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 +--
 interp/constrintern.ml          | 4 ++--
 test-suite/success/Notations2.v | 9 +++++++++
 3 files changed, 12 insertions(+), 4 deletions(-)

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
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index e14629df9b..1149cf1f58 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1071,11 +1071,11 @@ let find_appl_head_data c =
       c, impls, scopes, []
   | GApp (r, l) ->
     begin match DAst.get r with
-    | GRef (ref,_) when l != [] ->
+    | GRef (ref,_) ->
       let n = List.length l in
       let impls = implicits_of_global ref in
       let scopes = find_arguments_scope ref in
-        c, List.map (drop_first_implicits n) impls,
+        c, (if n = 0 then [] else List.map (drop_first_implicits n) impls),
         List.skipn_at_least n scopes,[]
     | _ -> c,[],[],[]
     end
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index 986908b7fc..dca0208fb0 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -185,3 +185,12 @@ Import A.
 Infix "+++" := Nat.add (at level 80).
 
 End M18.
+
+Module InheritanceArgumentScopes.
+
+Axiom p : forall (A:Type) (b:nat), A = A /\ b = b.
+Check fun A n => p (A * A) (n * n). (* safety check *)
+Notation q := @p.
+Check fun A n => q (A * A) (n * n). (* check that argument scopes are propagated *)
+
+End InheritanceArgumentScopes.
-- 
cgit v1.2.3