diff options
| author | Hugo Herbelin | 2020-04-13 14:00:32 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-12-09 11:04:47 +0100 |
| commit | da2ce98902f1843e5ff0f87ac773239020a70e0e (patch) | |
| tree | 800694d8af1ff8c20b1474522c8b9772d6584c36 /test-suite | |
| parent | ba1b3327a6040eaec8f5b58d339dcd6098abea81 (diff) | |
Constrintern: Code factorization in interning of record fields.
Also includes some fine-tuning of error messages.
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 5b67f632c9..b80345108e 100644 --- a/test-suite/output/RecordFieldErrors.out +++ b/test-suite/output/RecordFieldErrors.out @@ -11,4 +11,4 @@ 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. +unit: Not a projection. diff --git a/test-suite/output/RecordFieldErrors.v b/test-suite/output/RecordFieldErrors.v index 27aa07822b..ff817c31aa 100644 --- a/test-suite/output/RecordFieldErrors.v +++ b/test-suite/output/RecordFieldErrors.v @@ -35,4 +35,4 @@ acceptable and seems an unlikely mistake. *) Fail Check {| foo := tt; unit := tt |}. -(* unit: Not a projection of inductive t. *) +(* unit: Not a projection. *) |