diff options
| author | Matthieu Sozeau | 2016-05-25 15:17:28 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-07-06 14:38:05 +0200 |
| commit | f8a5cb590352a617de38fdd8ba5ffff7691d9841 (patch) | |
| tree | 5a4414e9e6d41fe0ebcccf5b25770b20bc31469d /test-suite | |
| parent | f77c2b488ca552b2316d4ebab1c051cb5a1347ab (diff) | |
Disallow dependent case on prim records w/o eta
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/primitiveproj.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v index b5e6ccd618..473d37eb36 100644 --- a/test-suite/success/primitiveproj.v +++ b/test-suite/success/primitiveproj.v @@ -47,7 +47,9 @@ Check _.(next) : option Y. Lemma eta_ind (y : Y) : y = Build_Y y.(next). Proof. Fail reflexivity. Abort. +Record Fdef := { Fa : nat ; Fb := Fa; Fc : nat }. +Scheme Fdef_rec := Induction for Fdef Sort Prop. (* Rules for parsing and printing of primitive projections and their eta expansions. |