Wish #1187 granted (support for canonical structures that are records

only up to some preliminary reductions)


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9166 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 0 deletions

diff --git a/test-suite/success/CanonicalStructure.v b/test-suite/success/CanonicalStructure.v
index 003810cc2..44d21b83b 100644
--- a/test-suite/success/CanonicalStructure.v
+++ b/test-suite/success/CanonicalStructure.v
@@ -5,3 +5,10 @@ Structure foo : Type := Foo {
 }.
 
 Canonical Structure unopt_nat := @Foo nat (fun _ => O).
+
+(* Granted wish #1187 *)
+
+Record Silly (X : Set) : Set := mkSilly { x : X }.
+Definition anotherMk := mkSilly.
+Definition struct := anotherMk nat 3.
+Canonical Structure struct.