From da2ce98902f1843e5ff0f87ac773239020a70e0e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 13 Apr 2020 14:00:32 +0200
Subject: Constrintern: Code factorization in interning of record fields.

Also includes some fine-tuning of error messages.
---
 test-suite/output/RecordFieldErrors.out | 2 +-
 test-suite/output/RecordFieldErrors.v   | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'test-suite')

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. *)
-- 
cgit v1.2.3