9 files changed, 54 insertions, 11 deletions
diff --git a/test-suite/bugs/closed/bug_12001.v b/test-suite/bugs/closed/bug_12001.v
new file mode 100644
index 0000000000..19533e49f1
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12001.v
@@ -0,0 +1,24 @@
+(* Argument names don't get mangled *)
+Set Mangle Names.
+Lemma leibniz_equiv_iff {A : Type} (x y : A) : True.
+Proof. tauto. Qed.
+Check leibniz_equiv_iff (A := nat) 2 3 : True.
+Unset Mangle Names.
+
+(* Coq doesn't make up names for arguments *)
+Definition bar (a a : nat) : nat := 3.
+Arguments bar _ _ : assert.
+Fail Arguments bar a a0 : assert.
+
+(* This definition caused an anomaly in a version of this PR
+without the change to prepare_implicits *)
+Set Implicit Arguments.
+Definition foo (_ : nat) (_ : @eq nat ltac:(assumption) 2) : True := I.
+Fail Check foo (H := 2).
+
+Definition baz (a b : nat) := b.
+Arguments baz a {b}.
+Set Mangle Names.
+Definition baz2 (a b : nat) := b.
+Arguments baz2 a {b}.
+Unset Mangle Names.
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index e0aa758812..c28bb14eb3 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -84,8 +84,6 @@ Argument lists should agree on the names they provide.
 The command has indeed failed with message:
 Sequences of implicit arguments must be of different lengths.
 The command has indeed failed with message:
-Some argument names are duplicated: F
-The command has indeed failed with message:
 Argument number 3 is a trailing implicit, so it can't be declared non
 maximal. Please use { } instead of [ ].
 The command has indeed failed with message:
diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v
index 6ac09cf771..6001850046 100644
--- a/test-suite/output/Arguments_renaming.v
+++ b/test-suite/output/Arguments_renaming.v
@@ -48,7 +48,6 @@ Check @myplus.
 
 Fail Arguments eq_refl {F g}, [H] k.
 Fail Arguments eq_refl {F}, [F] : rename.
-Fail Arguments eq_refl {F F}, [F] F : rename.
 Fail Arguments eq {A} x [z] : rename.
 Fail Arguments eq {F} x z y.
 Fail Arguments eq {R} s t.
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index ef7667936c..2265028d3e 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -5,7 +5,7 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I
 d2 = fun x : nat => d1 (y:=x)
      : forall x x0 : nat, x0 = x -> x0 = x
 
-Arguments d2 [x x0]%nat_scope
+Arguments d2 [x x]%nat_scope
 map id (1 :: nil)
      : list nat
 map id' (1 :: nil)
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.
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 563651cfa5..7acaa92b89 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -190,7 +190,7 @@ Record Monad {m : Type -> Type} := {
 
 Print Visibility.
 Print unit.
-Arguments unit {m m0 α}.
+Arguments unit {m _ α}.
 Arguments Monad : clear implicits.
 Notation "'return' t" := (unit t).