Merge PR #8737: Correctly report non-projection fields in records

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..5b67f632c9
--- /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 both t and t'.
+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..27aa07822b
--- /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 both t and t'. *)
+
+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. *)