Fixes #13413: freshness issue with "%" introduction pattern.

We build earlier the final expected name at the end of a sequence of
"%" introduction patterns.

3 files changed, 47 insertions, 17 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b40bdbc25e..276c090778 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2324,11 +2324,6 @@ let rewrite_hyp_then with_evars thin l2r id tac =
     tclEVARSTHEN sigma (Tacticals.New.tclTHENFIRST eqtac (tac thin))
   end
 
-let prepare_naming ?loc = function
-  | IntroIdentifier id -> NamingMustBe (CAst.make ?loc id)
-  | IntroAnonymous -> NamingAvoid Id.Set.empty
-  | IntroFresh id -> NamingBasedOn (id, Id.Set.empty)
-
 let rec explicit_intro_names = let open CAst in function
 | {v=IntroForthcoming _} :: l -> explicit_intro_names l
 | {v=IntroNaming (IntroIdentifier id)} :: l -> Id.Set.add id (explicit_intro_names l)
@@ -2383,7 +2378,12 @@ let check_thin_clash_then id thin avoid tac =
   else
     tac thin
 
-let make_tmp_naming avoid l = function
+let make_naming ?loc avoid l = function
+  | IntroIdentifier id -> NamingMustBe (CAst.make ?loc id)
+  | IntroAnonymous -> NamingAvoid (Id.Set.union avoid (explicit_intro_names l))
+  | IntroFresh id -> NamingBasedOn (id, Id.Set.union avoid (explicit_intro_names l))
+
+let rec make_naming_action avoid l = function
   (* In theory, we could use a tmp id like "wild_id" for all actions
      but we prefer to avoid it to avoid this kind of "ugly" names *)
   (* Alternatively, we could have called check_thin_clash_then on
@@ -2391,7 +2391,16 @@ 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, Id.Set.union avoid (explicit_intro_names l))
-  | pat -> NamingAvoid(Id.Set.union avoid (explicit_intro_names ((CAst.make @@ IntroAction pat)::l)))
+  | IntroApplyOn (_,{CAst.v=pat;loc}) -> make_naming_pattern avoid ?loc l pat
+  | (IntroOrAndPattern _ | IntroInjection _ | IntroRewrite _) as pat ->
+    NamingAvoid(Id.Set.union avoid (explicit_intro_names ((CAst.make @@ IntroAction pat)::l)))
+
+and make_naming_pattern ?loc avoid l = function
+  | IntroNaming pat -> make_naming ?loc avoid l pat
+  | IntroAction pat -> make_naming_action avoid l pat
+  | IntroForthcoming _ -> NamingAvoid (Id.Set.union avoid (explicit_intro_names l))
+
+let prepare_naming ?loc pat = make_naming ?loc Id.Set.empty [] pat
 
 let fit_bound n = function
   | None -> true
@@ -2437,7 +2446,7 @@ let rec intro_patterns_core with_evars avoid ids thin destopt bound n tac =
         (fun ids -> intro_patterns_core with_evars avoid ids thin destopt bound
           (n+List.length ids) tac l)
   | IntroAction pat ->
-      intro_then_gen (make_tmp_naming avoid l pat)
+      intro_then_gen (make_naming_action avoid l pat)
         destopt true false
         (intro_pattern_action ?loc with_evars pat thin destopt
           (fun thin bound' -> intro_patterns_core with_evars avoid ids thin destopt bound' 0
@@ -2474,24 +2483,21 @@ and intro_pattern_action ?loc with_evars pat thin destopt tac id =
   | IntroRewrite l2r ->
       rewrite_hyp_then with_evars thin l2r id (fun thin -> tac thin None [])
   | IntroApplyOn ({CAst.loc=loc';v=f},{CAst.loc;v=pat}) ->
-      let naming,tac_ipat =
+      let naming = NamingMustBe (CAst.make ?loc id) in
+      let _,tac_ipat =
         prepare_intros ?loc with_evars (IntroIdentifier id) destopt pat in
-      let doclear =
-        if naming = NamingMustBe (CAst.make ?loc id) then
-          Proofview.tclUNIT () (* apply_in_once do a replacement *)
-        else
-          clear [id] in
       let f env sigma = let (sigma, c) = f env sigma in (sigma,(c, NoBindings))
       in
       apply_in_delayed_once true true with_evars naming id (None,CAst.make ?loc:loc' f)
-        (fun id -> Tacticals.New.tclTHENLIST [doclear; tac_ipat id; tac thin None []])
+        (fun id -> Tacticals.New.tclTHENLIST [tac_ipat id; tac thin None []])
 
 and prepare_intros ?loc with_evars dft destopt = function
   | IntroNaming ipat ->
       prepare_naming ?loc ipat,
-      (fun id -> move_hyp id destopt)
+      (fun _ -> Proofview.tclUNIT ())
   | IntroAction ipat ->
-      prepare_naming ?loc dft,
+      (* Special case for apply in which clears iff it is a replacement *)
+      (match dft with IntroIdentifier _ -> prepare_naming ?loc dft | _ -> make_naming_action Id.Set.empty [] ipat),
       (let tac thin bound =
         intro_patterns_core with_evars Id.Set.empty [] thin destopt bound 0
           (fun _ l -> clear_wildcards l) in
diff --git a/test-suite/bugs/closed/bug_13413.v b/test-suite/bugs/closed/bug_13413.v
new file mode 100644
index 0000000000..b4414a6a1d
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13413.v
@@ -0,0 +1,20 @@
+Goal forall (A B : Prop) (H : A -> B), A -> A -> B.
+intros A B H ?%H H0.
+exact H1.
+Qed.
+
+Goal forall (A B : Prop) (H : A -> B), A -> A -> B.
+intros A B H ?H%H H0.
+exact H1.
+Qed.
+
+Goal forall (A B : Prop) (H : A -> B), A -> A -> B.
+intros A B H J%H H0.
+exact J.
+Qed.
+
+Set Mangle Names.
+Goal forall (A B : Prop) (H : A -> B), A -> A -> B.
+intros A B H ?%H _0.
+assumption.
+Qed.
diff --git a/test-suite/success/forward.v b/test-suite/success/forward.v
index 4e36dec15b..62c788e910 100644
--- a/test-suite/success/forward.v
+++ b/test-suite/success/forward.v
@@ -27,3 +27,7 @@ Fail match goal with |- (?f ?a) => idtac end. (* should be beta-iota reduced *)
 2:match goal with _: (?f ?a) |- _ => idtac end. (* should not be beta-iota reduced *)
 Abort.
 
+Goal nat.
+assert nat as J%S by exact 0.
+exact J.
+Qed.