diff options
Diffstat (limited to 'test-suite/success/Record.v')
| -rw-r--r-- | test-suite/success/Record.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v index d9ad721a0..885fff483 100644 --- a/test-suite/success/Record.v +++ b/test-suite/success/Record.v @@ -46,7 +46,7 @@ Qed. (* Correct type inference of record notation. Initial example by Spiwack. *) -Record Machin := { +Inductive Machin := { Bazar : option Machin }. |