Do not refresh the names of implicit arguments.

Try just going with the user-given names, and not worrying about
what happens with repeated names or anonymous implicits.
(Support for anonymous implicits is due to herbelin in #11098.)

This PR should not change behaviour in the absence of repeated names.
Since repeated names are already a poorly handled corner case, I would
recommend changing binder names to avoid overlap in the case of a
change in behavior.

Since anonymous implicits and implicits with repeated names can already
happen, I think this is unlikely to cause too many new problems,
though it might exacerbate existing ones. However, I already had to fix
one newly possible anomaly, so I can't be too confident.

The most common change in external developments was that an argument
no longer gets `0` appended to it, causing the `Arguments` command
to complain about renaming.
To fix this and keep the old name, one can simply use the `rename` flag
as suggested, or switch to the new, un-suffixed name.

Closes #6785
Closes #12001

Another step towards checking the standard library with `-mangle-names`.

1 files changed, 0 insertions, 8 deletions

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