Imported Upstream version 8.5~beta1+dfsg

1 files changed, 14 insertions, 0 deletions

diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v
index a79d28fa..43e3493c 100644
--- a/test-suite/success/Scopes.v
+++ b/test-suite/success/Scopes.v
@@ -6,3 +6,17 @@ Module A.
 Definition opp := Z.opp.
 End A.
 Check (A.opp 3).
+
+(* Test extra scopes to be used in the presence of coercions *)
+
+Record B := { f :> Z -> Z }.
+Variable a:B.
+Arguments Scope a [Z_scope].
+Check a 0.
+
+(* Check that casts activate scopes if ever possible *)
+
+Inductive U := A.
+Bind Scope u with U.
+Notation "'ε'" := A : u.
+Definition c := ε : U.