Standardize handling of Automatic Introduction.

This fixes #8791.
We explicitly specify for intro the names of binders which are
given by the user. This still can suffer from spurious collisions,
see #8819.

1 files changed, 9 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_8791.v b/test-suite/bugs/closed/bug_8791.v
new file mode 100644
index 0000000000..9be1936cdf
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8791.v
@@ -0,0 +1,9 @@
+Class Inhabited (A : Type) : Type := populate { inhabitant : A }.
+
+Definition A := 42.
+
+Instance foo (A: Type): Inhabited (list A).
+Check A.
+Abort.
+
+Fail Instance foo (A : nat) (A : Type) : Inhabited nat.