From bfae260f7ba026e17e0cc599b8507bd133c4edc0 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 22 Nov 2019 10:40:40 +0100
Subject: [CS] support #[local] attribute

---
 test-suite/success/CanonicalStructure.v | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

(limited to 'test-suite')

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.
-- 
cgit v1.2.3