Merge PR #11162: [CS] support #[local] attribute

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: maximedenes

1 files changed, 22 insertions, 0 deletions

diff --git a/test-suite/success/CanonicalStructure.v b/test-suite/success/CanonicalStructure.v
index b8cae47196..e6d674c1e6 100644
--- a/test-suite/success/CanonicalStructure.v
+++ b/test-suite/success/CanonicalStructure.v
@@ -29,3 +29,25 @@ Canonical Structure bool_test := mk_test (fun x y => x || y).
 Definition b := bool.
 
 Check (fun x : b => x != x).
+
+Inductive four := x0 | x1 | x2 | x3.
+Structure local := MKL { l : four }.
+
+Section X.
+  Definition s0 := MKL x0.
+  #[local] Canonical Structure s0.
+  Check (refl_equal _ : l _ = x0).
+
+  #[local] Canonical Structure s1 := MKL x1.
+  Check (refl_equal _ : l _ = x1).
+
+  Local Canonical Structure s2 := MKL x2.
+  Check (refl_equal _ : l _ = x2).
+
+End X.
+Fail Check (refl_equal _ : l _ = x0).
+Fail Check (refl_equal _ : l _ = x1).
+Fail Check (refl_equal _ : l _ = x2).
+Check s0.
+Check s1.
+Check s2.