diff options
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 |}. |