9 files changed, 54 insertions, 33 deletions
diff --git a/dev/ci/user-overlays/12756-jashug-dont-refresh-argument-names.sh b/dev/ci/user-overlays/12756-jashug-dont-refresh-argument-names.sh
new file mode 100644
index 0000000000..54fdd87566
--- /dev/null
+++ b/dev/ci/user-overlays/12756-jashug-dont-refresh-argument-names.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "12756" ] || [ "$CI_BRANCH" = "dont-refresh-argument-names" ]; then
+
+    mathcomp_CI_REF=dont-refresh-argument-names-overlay
+    mathcomp_CI_GITURL=https://github.com/jashug/math-comp
+
+    oddorder_CI_REF=dont-refresh-argument-names-overlay
+    oddorder_CI_GITURL=https://github.com/jashug/odd-order
+
+fi
diff --git a/doc/changelog/02-specification-language/12756-dont-refresh-argument-names.rst b/doc/changelog/02-specification-language/12756-dont-refresh-argument-names.rst
new file mode 100644
index 0000000000..b0cf4ca4e3
--- /dev/null
+++ b/doc/changelog/02-specification-language/12756-dont-refresh-argument-names.rst
@@ -0,0 +1,9 @@
+- **Changed:**
+  Tweaked the algorithm giving default names to arguments.
+  Should reduce the frequency that argument names get an
+  unexpected suffix.
+  Also makes :flag:`Mangle Names` not mess up argument names.
+  (`#12756 <https://github.com/coq/coq/pull/12756>`_,
+  fixes `#12001 <https://github.com/coq/coq/issues/12001>`_
+  and `#6785 <https://github.com/coq/coq/issues/6785>`_,
+  by Jasper Hugunin).
diff --git a/interp/impargs.ml b/interp/impargs.ml
index db102470b0..48961c6c8a 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -20,7 +20,6 @@ open Lib
 open Libobject
 open EConstr
 open Reductionops
-open Namegen
 open Constrexpr
 
 module NamedDecl = Context.Named.Declaration
@@ -247,24 +246,15 @@ let is_rigid env sigma t =
      is_rigid_head sigma t
   | _ -> true
 
-let find_displayed_name_in sigma all avoid na (env, b) =
-  let envnames_b = (env, b) in
-  let flag = RenamingElsewhereFor envnames_b in
-  if all then compute_and_force_displayed_name_in sigma flag avoid na b
-  else compute_displayed_name_in sigma flag avoid na b
-
-let compute_implicits_names_gen all env sigma t =
+let compute_implicits_names env sigma t =
   let open Context.Rel.Declaration in
-  let rec aux env avoid names t =
+  let rec aux env names t =
     let t = whd_all env sigma t in
     match kind sigma t with
     | Prod (na,a,b) ->
-       let na',avoid' = find_displayed_name_in sigma all avoid na.Context.binder_name (names,b) in
-       aux (push_rel (LocalAssum (na,a)) env) avoid' (na'::names) b
+       aux (push_rel (LocalAssum (na,a)) env) (na.Context.binder_name::names) b
     | _ -> List.rev names
-  in aux env Id.Set.empty [] t
-
-let compute_implicits_names = compute_implicits_names_gen true
+  in aux env [] t
 
 let compute_implicits_explanation_gen strict strongly_strict revpat contextual env sigma t =
   let open Context.Rel.Declaration in
@@ -291,9 +281,9 @@ let compute_implicits_explanation_flags env sigma f t =
     (f.strict || f.strongly_strict) f.strongly_strict
     f.reversible_pattern f.contextual env sigma t
 
-let compute_implicits_flags env sigma f all t =
+let compute_implicits_flags env sigma f t =
   List.combine
-    (compute_implicits_names_gen all env sigma t)
+    (compute_implicits_names env sigma t)
     (compute_implicits_explanation_flags env sigma f t)
 
 let compute_auto_implicits env sigma flags enriching t =
@@ -361,10 +351,10 @@ let positions_of_implicits (_,impls) =
 
 let rec prepare_implicits i f = function
   | [] -> []
-  | (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit.")
-  | (Name id, Some imp)::imps ->
+  | (na, Some imp)::imps ->
       let imps' = prepare_implicits (i+1) f imps in
-      Some (ExplByName id,imp,(set_maximality Silent (Name id) i imps' f.maximal,true)) :: imps'
+      let expl = match na with Name id -> ExplByName id | Anonymous -> ExplByPos (i,None) in
+      Some (expl,imp,(set_maximality Silent na i imps' f.maximal,true)) :: imps'
   | _::imps -> None :: prepare_implicits (i+1) f imps
 
 let set_manual_implicits silent flags enriching autoimps l =
@@ -393,7 +383,7 @@ let set_manual_implicits silent flags enriching autoimps l =
 
 let compute_semi_auto_implicits env sigma f t =
   if not f.auto then [DefaultImpArgs, []]
-  else let l = compute_implicits_flags env sigma f false t in
+  else let l = compute_implicits_flags env sigma f t in
        [DefaultImpArgs, prepare_implicits 1 f l]
 
 (*s Constants. *)
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/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).
 
diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml
index 360e228bfc..be9cc059a7 100644
--- a/vernac/comArguments.ml
+++ b/vernac/comArguments.ml
@@ -213,14 +213,6 @@ let vernac_arguments ~section_local reference args more_implicits flags =
     in CErrors.user_err ~hdr:"vernac_declare_arguments" msg
   end;
 
-  let duplicate_names =
-    List.duplicates Name.equal (List.filter ((!=) Anonymous) names)
-  in
-  if not (List.is_empty duplicate_names) then begin
-    CErrors.user_err Pp.(strbrk "Some argument names are duplicated: " ++
-                         prlist_with_sep pr_comma Name.print duplicate_names)
-  end;
-
   let implicits =
     List.map (fun { name; implicit_status = i } -> (name,i)) args
   in