8 files changed, 42 insertions, 7 deletions

diff --git a/test-suite/bugs/closed/bug_12763.v b/test-suite/bugs/closed/bug_12763.v
new file mode 100644
index 0000000000..6cbcc0d3b0
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12763.v
@@ -0,0 +1,6 @@
+Inductive bool_list := S (y : bool) (l : bool_list) | O.
+Scheme Equality for bool_list.
+
+Set Mangle Names.
+Scheme Equality for nat.
+Scheme Equality for list.
diff --git a/test-suite/output/ErrorLocation_12774_3.out b/test-suite/output/ErrorLocation_12774_3.out
new file mode 100644
index 0000000000..dbd3dbd1e2
--- /dev/null
+++ b/test-suite/output/ErrorLocation_12774_3.out
@@ -0,0 +1,3 @@
+File "stdin", line 3, characters 0-1:
+Error: No product even after head-reduction.
+
diff --git a/test-suite/output/ErrorLocation_12774_3.v b/test-suite/output/ErrorLocation_12774_3.v
new file mode 100644
index 0000000000..c624402a81
--- /dev/null
+++ b/test-suite/output/ErrorLocation_12774_3.v
@@ -0,0 +1,4 @@
+Ltac f := auto; intro.
+Goal False.
+f.
+Abort.
diff --git a/test-suite/output/Error_msg_diffs.out b/test-suite/output/Error_msg_diffs.out
index 3e337e892d..2645524a70 100644
--- a/test-suite/output/Error_msg_diffs.out
+++ b/test-suite/output/Error_msg_diffs.out
@@ -1,4 +1,4 @@
-File "stdin", line 32, characters 0-12:
+File "stdin", line 32, characters 0-11:
 Error:
 In environment
 T : Type
diff --git a/test-suite/output/RecordMissingField.out b/test-suite/output/RecordMissingField.out
index 7c80a6065f..28beee90b2 100644
--- a/test-suite/output/RecordMissingField.out
+++ b/test-suite/output/RecordMissingField.out
@@ -1,4 +1,16 @@
-File "stdin", line 8, characters 5-22:
-Error: Cannot infer field y2p of record point2d in environment:
-p : point2d
-
+The command has indeed failed with message:
+The following term contains unresolved implicit arguments:
+  (fun p : point2d => {| x2p := x2p p + 1; y2p := ?y2p |})
+More precisely: 
+- ?y2p: Cannot infer field y2p of record point2d in environment:
+  p : point2d
+The command has indeed failed with message:
+The following term contains unresolved implicit arguments:
+  (fun p : point2d => {| x2p := x2p p + (fun n : nat => ?n) 1; y2p := ?y2p |})
+More precisely: 
+- ?n: Cannot infer this placeholder of type "nat" in
+  environment:
+  p : point2d
+  n : nat
+- ?y2p: Cannot infer field y2p of record point2d in environment:
+  p : point2d
diff --git a/test-suite/output/RecordMissingField.v b/test-suite/output/RecordMissingField.v
index 84f1748fa0..8ca721564b 100644
--- a/test-suite/output/RecordMissingField.v
+++ b/test-suite/output/RecordMissingField.v
@@ -3,6 +3,10 @@ should contain missing field, and the inferred type of the record **)
 
 Record point2d := mkPoint { x2p: nat; y2p: nat }.
 
-
-Definition increment_x (p: point2d) : point2d :=
+Fail Definition increment_x (p: point2d) : point2d :=
   {| x2p := x2p p + 1; |}.
+
+(* Here there is also an unresolved implicit, which should give an
+   understadable error as well *)
+Fail Definition increment_x (p: point2d) : point2d :=
+  {| x2p := x2p p + (fun n => _) 1; |}.
diff --git a/test-suite/output/ssr_error_multiple_intro_after_case.out b/test-suite/output/ssr_error_multiple_intro_after_case.out
new file mode 100644
index 0000000000..51fb208ae9
--- /dev/null
+++ b/test-suite/output/ssr_error_multiple_intro_after_case.out
@@ -0,0 +1,3 @@
+File "stdin", line 3, characters 0-11:
+Error: x already used
+
diff --git a/test-suite/output/ssr_error_multiple_intro_after_case.v b/test-suite/output/ssr_error_multiple_intro_after_case.v
new file mode 100644
index 0000000000..1f87966693
--- /dev/null
+++ b/test-suite/output/ssr_error_multiple_intro_after_case.v
@@ -0,0 +1,3 @@
+Require Import ssreflect.
+Goal forall p : nat * nat , True.
+case => x x.