Merge PR #11164: [CS] allow Let variable to be canonical

Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: ppedrot

1 files changed, 19 insertions, 0 deletions

diff --git a/test-suite/success/CanonicalStructure.v b/test-suite/success/CanonicalStructure.v
index e6d674c1e6..88702a6e80 100644
--- a/test-suite/success/CanonicalStructure.v
+++ b/test-suite/success/CanonicalStructure.v
@@ -51,3 +51,22 @@ Fail Check (refl_equal _ : l _ = x2).
 Check s0.
 Check s1.
 Check s2.
+
+Section Y.
+  Let s3 := MKL x3.
+  Canonical Structure s3.
+  Check (refl_equal _ : l _ = x3).
+End Y.
+Fail Check (refl_equal _ : l _ = x3).
+Fail Check s3.
+
+Section V.
+  #[canonical] Let s3 := MKL x3.
+  Check (refl_equal _ : l _ = x3).
+End V.
+
+Section W.
+  #[canonical, local] Definition s2' := MKL x2.
+  Check (refl_equal _ : l _ = x2).
+End W.
+Fail Check (refl_equal _ : l _ = x2).