Fixing incomplete bugfix in 76f27140e6e34 (unfortunately 5 commits

ago) which broke compilation of theories/Logic/WKL.v (collision
between a temporary name and a user name).

2 files changed, 11 insertions, 1 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index bbee0a2a79..0235126cc0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2122,7 +2122,7 @@ let make_tmp_naming avoid l = function
      case of IntroFresh, we should use check_thin_clash_then anyway to
      prevent the case of an IntroFresh precisely using the wild_id *)
   | IntroWildcard -> NamingBasedOn (wild_id,avoid@explicit_intro_names l)
-  | _ -> NamingAvoid(avoid@explicit_intro_names l)
+  | pat -> NamingAvoid(avoid@explicit_intro_names ((dloc,IntroAction pat)::l))
 
 let fit_bound n = function
   | None -> true
diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index 4959b65788..ae1694c58c 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -51,3 +51,13 @@ Fail clear H0.
 match goal with H:_ |- _ => clear H end. (* clear H1:False *)
 match goal with H:_ |- _ => exact H end. (* check that next hyp shows 0=0 *)
 Qed.
+
+Goal (True -> 0=0) -> True -> 0=0.
+intros H H1/H.
+exact H1.
+Qed.
+
+Goal forall n, n = S n -> 0=0.
+intros n H/n_Sn.
+destruct H.
+Qed.