4 files changed, 58 insertions, 0 deletions
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index cef7d1a702..46784d1897 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -1,5 +1,7 @@
 [< 0 > + < 1 > * < 2 >]
      : nat
+[< b > + < b > * < 2 >]
+     : nat
 [<< # 0 >>]
      : option nat
 [1 {f 1}]
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 9738ce5a5e..6bdbf1bed5 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -10,6 +10,10 @@ Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4).
 Notation "< x >" := x (in custom myconstr at level 3, x constr at level 10).
 Check [ < 0 > + < 1 > * < 2 >].
 
+Axiom a : nat.
+Notation b := a.
+Check [ < b > + < a > * < 2 >].
+
 Declare Custom Entry anotherconstr.
 
 Notation "[ x ]" := x (x custom myconstr at level 6).
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. *)