blob: 44d21b83bc4babbecc858cb7b62a45649d9be0ec (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
(* Bug #1172 *)
Structure foo : Type := Foo {
A : Set; Aopt := option A; unopt : Aopt -> A
}.
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.
|
