diff options
| author | Tej Chajed | 2018-10-23 10:28:48 -0400 |
|---|---|---|
| committer | Tej Chajed | 2018-10-26 09:55:17 -0400 |
| commit | fcde9195f8e63ff427c03af6373f344c991fb099 (patch) | |
| tree | bbc1b8fdec678ef21bc87b3af1107701e155656d /test-suite | |
| parent | 3059b9fa7c2f0e8d0d7eadabfdb5d833f294a904 (diff) | |
Add record names to multiple records error message
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/RecordFieldErrors.out | 2 | ||||
| -rw-r--r-- | test-suite/output/RecordFieldErrors.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/output/RecordFieldErrors.out b/test-suite/output/RecordFieldErrors.out index 7bf668ad86..5b67f632c9 100644 --- a/test-suite/output/RecordFieldErrors.out +++ b/test-suite/output/RecordFieldErrors.out @@ -3,7 +3,7 @@ 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. +This record contains fields of both t and t'. The command has indeed failed with message: unit: Not a projection. The command has indeed failed with message: diff --git a/test-suite/output/RecordFieldErrors.v b/test-suite/output/RecordFieldErrors.v index f28fab410b..27aa07822b 100644 --- a/test-suite/output/RecordFieldErrors.v +++ b/test-suite/output/RecordFieldErrors.v @@ -16,7 +16,7 @@ Fail Check {| unit := tt; Fail Check {| foo := tt; bar := tt |}. -(* This record contains fields of different records. *) +(* This record contains fields of both t and t'. *) Fail Check {| unit := tt; unit := tt |}. |