diff options
| author | Tej Chajed | 2018-10-15 17:00:09 -0400 |
|---|---|---|
| committer | Tej Chajed | 2018-10-26 09:55:16 -0400 |
| commit | 3059b9fa7c2f0e8d0d7eadabfdb5d833f294a904 (patch) | |
| tree | 6bf03b1ae3a01b88494c04f569c939768e318d7d /test-suite | |
| parent | 27266c1f79e565a6a19da4c79fc1ce83f748e31c (diff) | |
Correctly report non-projection fields in records
Fixes #8736.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/RecordFieldErrors.out | 14 | ||||
| -rw-r--r-- | test-suite/output/RecordFieldErrors.v | 38 |
2 files changed, 52 insertions, 0 deletions
diff --git a/test-suite/output/RecordFieldErrors.out b/test-suite/output/RecordFieldErrors.out new file mode 100644 index 0000000000..7bf668ad86 --- /dev/null +++ b/test-suite/output/RecordFieldErrors.out @@ -0,0 +1,14 @@ +The command has indeed failed with message: +unit: Not a projection. +The command has indeed failed with message: +unit: Not a projection. +The command has indeed failed with message: +This record contains fields of different records. +The command has indeed failed with message: +unit: Not a projection. +The command has indeed failed with message: +This record defines several times the field foo. +The command has indeed failed with message: +This record defines several times the field unit. +The command has indeed failed with message: +unit: Not a projection of inductive t. diff --git a/test-suite/output/RecordFieldErrors.v b/test-suite/output/RecordFieldErrors.v new file mode 100644 index 0000000000..f28fab410b --- /dev/null +++ b/test-suite/output/RecordFieldErrors.v @@ -0,0 +1,38 @@ +(** Check that various errors in record fields are reported with the correct +underlying issue. *) + +Record t := + { foo: unit }. + +Record t' := + { bar: unit }. + +Fail Check {| unit := tt |}. +(* unit: Not a projection. *) + +Fail Check {| unit := tt; + foo := tt |}. +(* unit: Not a projection. *) + +Fail Check {| foo := tt; + bar := tt |}. +(* This record contains fields of different records. *) + +Fail Check {| unit := tt; + unit := tt |}. +(* unit: Not a projection. *) + +Fail Check {| foo := tt; + foo := tt |}. +(* This record defines several times the field foo. *) + +Fail Check {| foo := tt; + unit := tt; + unit := tt |}. +(* This is slightly wrong (would prefer "unit: Not a projection."), but it's +acceptable and seems an unlikely mistake. *) +(* This record defines several times the field unit. *) + +Fail Check {| foo := tt; + unit := tt |}. +(* unit: Not a projection of inductive t. *) |