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, 9 insertions, 0 deletions

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).