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.
---
 test-suite/success/Notations2.v | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'test-suite')

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