Avoid explicit names in binders for automatic intros

3 files changed, 15 insertions, 3 deletions

diff --git a/CHANGES.md b/CHANGES.md
index 4fafb9a18a..fe9f758597 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -90,6 +90,9 @@ Vernacular commands
 
 - `Arguments` now accepts names for arguments provided with `extra_scopes`.
 
+- The naming scheme for anonymous binders in a `Theorem` has changed to
+  avoid conflicts with explicitly named binders.
+
 Tools
 
 - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values:
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 9e9d52b72c..5b1d7dabba 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1063,9 +1063,16 @@ let intros_replacing ids =
 
 (* The standard for implementing Automatic Introduction *)
 let auto_intros_tac ids =
-  Tacticals.New.tclMAP (function
-      | Name id -> intro_mustbe_force id
-      | Anonymous -> intro) (List.rev ids)
+  let fold used = function
+    | Name id -> Id.Set.add id used
+    | Anonymous -> used
+  in
+  let avoid = NamingAvoid (List.fold_left fold Id.Set.empty ids) in
+  let naming = function
+    | Name id -> NamingMustBe CAst.(make id)
+    | Anonymous -> avoid
+  in
+  Tacticals.New.tclMAP (fun name -> intro_gen (naming name) MoveLast true false) (List.rev ids)
 
 (* User-level introduction tactics *)
 
diff --git a/test-suite/bugs/closed/bug_8819.v b/test-suite/bugs/closed/bug_8819.v
new file mode 100644
index 0000000000..a4cb9dcd14
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8819.v
@@ -0,0 +1,2 @@
+Theorem foo (_ : nat) (H : bool) : bool.
+Proof. exact H. Qed.