From 300157fc6176856f3f792d956925af366ef3329e Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Wed, 19 Aug 2020 08:13:08 -0700
Subject: 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`.
---
 test-suite/bugs/closed/bug_12001.v | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_12001.v

(limited to 'test-suite/bugs')

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.
-- 
cgit v1.2.3