From e56c65cf68c4055b4e1272b5a2afbf5803d93a42 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 28 Nov 2020 15:10:21 +0100 Subject: Fixes #13413: freshness issue with "%" introduction pattern. We build earlier the final expected name at the end of a sequence of "%" introduction patterns. --- tactics/tactics.ml | 40 ++++++++++++++++++++++---------------- test-suite/bugs/closed/bug_13413.v | 20 +++++++++++++++++++ test-suite/success/forward.v | 4 ++++ 3 files changed, 47 insertions(+), 17 deletions(-) create mode 100644 test-suite/bugs/closed/bug_13413.v 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. -- cgit v1.2.3 From 861c22919da6877b91ed5a095e6b0e95725ca225 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 28 Nov 2020 15:12:55 +0100 Subject: Small reworking of code in intros-pattern. We compute earlier if "apply in" clears or not. We inline prepare_naming into its only client prepare_intros_opt (using the more general make_naming instead). --- tactics/tactics.ml | 44 ++++++++++++++++++++++++-------------------- 1 file changed, 24 insertions(+), 20 deletions(-) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 276c090778..09627b15c4 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1299,7 +1299,7 @@ let do_replace id = function [Ti] and the first one (resp last one) being [G] whose hypothesis [id] is replaced by P using the proof given by [tac] *) -let clenv_refine_in ?err with_evars targetid id sigma0 clenv tac = +let clenv_refine_in ?err with_evars targetid replace sigma0 clenv tac = let clenv = Clenv.clenv_pose_dependent_evars ~with_evars clenv in let evd = Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd in let clenv = Clenv.update_clenv_evd clenv evd in @@ -1310,11 +1310,10 @@ let clenv_refine_in ?err with_evars targetid id sigma0 clenv tac = let new_hyp_prf = clenv_value clenv in let exact_tac = Logic.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf) in let naming = NamingMustBe (CAst.make targetid) in - let with_clear = do_replace (Some id) naming in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS (clear_metas evd)) (Tacticals.New.tclTHENLAST - (assert_after_then_gen ?err with_clear naming new_hyp_typ tac) exact_tac) + (assert_after_then_gen ?err replace naming new_hyp_typ tac) exact_tac) (********************************************) (* Elimination tactics *) @@ -1365,7 +1364,7 @@ let elimination_in_clause_scheme env sigma with_evars ~flags if EConstr.eq_constr sigma hyp_typ new_hyp_typ then user_err ~hdr:"general_rewrite_in" (str "Nothing to rewrite in " ++ Id.print id ++ str"."); - clenv_refine_in with_evars id id sigma elimclause'' + clenv_refine_in with_evars id true sigma elimclause'' (fun id -> Proofview.tclUNIT ()) (* @@ -1814,6 +1813,7 @@ let apply_in_once ?(respect_opaque = false) with_delta let t' = Tacmach.New.pf_get_hyp_typ id gl in let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in let targetid = find_name true (LocalAssum (make_annot Anonymous Sorts.Relevant,t')) naming gl in + let replace = Id.equal id targetid in let rec aux ?err idstoclear with_destruct c = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in @@ -1826,7 +1826,7 @@ let apply_in_once ?(respect_opaque = false) with_delta if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in try let clause = apply_in_once_main flags innerclause env sigma (loc,c,lbind) in - clenv_refine_in ?err with_evars targetid id sigma clause + clenv_refine_in ?err with_evars targetid replace sigma clause (fun id -> replace_error_option err ( apply_clear_request clear_flag false c <*> @@ -2484,20 +2484,15 @@ and intro_pattern_action ?loc with_evars pat thin destopt tac id = 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 = NamingMustBe (CAst.make ?loc id) in - let _,tac_ipat = - prepare_intros ?loc with_evars (IntroIdentifier id) destopt pat in - let f env sigma = let (sigma, c) = f env sigma in (sigma,(c, NoBindings)) - in + let tac_ipat = prepare_action ?loc with_evars destopt pat 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 [tac_ipat id; tac thin None []]) -and prepare_intros ?loc with_evars dft destopt = function +and prepare_action ?loc with_evars destopt = function | IntroNaming ipat -> - prepare_naming ?loc ipat, (fun _ -> Proofview.tclUNIT ()) | IntroAction ipat -> - (* 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 @@ -2534,9 +2529,19 @@ let intros_patterns with_evars = function (* Forward reasoning *) (**************************) -let prepare_intros_opt with_evars dft destopt = function - | None -> prepare_naming dft, (fun _id -> Proofview.tclUNIT ()) - | Some {CAst.loc;v=ipat} -> prepare_intros ?loc with_evars dft destopt ipat +let prepare_intros_opt with_evars dft destopt ipat = + let naming, loc, ipat = match ipat with + | None -> + let pat = IntroNaming dft in make_naming_pattern Id.Set.empty [] pat, None, pat + | Some {CAst.loc;v=(IntroNaming pat as ipat)} -> + (* "apply ... in H as id" needs to use id and H is kept iff id<>H *) + prepare_naming ?loc pat, loc, ipat + | Some {CAst.loc;v=(IntroAction pat as ipat)} -> + (* "apply ... in H as pat" reuses H so that old H is always cleared *) + (match dft with IntroIdentifier _ -> prepare_naming ?loc dft | _ -> make_naming_action Id.Set.empty [] pat), + loc, ipat + | Some {CAst.loc;v=(IntroForthcoming _)} -> assert false in + naming, prepare_action ?loc with_evars destopt ipat let ipat_of_name = function | Anonymous -> None @@ -3051,8 +3056,7 @@ let specialize (c,lbind) ipat = match EConstr.kind sigma (fst(EConstr.decompose_app sigma (snd(EConstr.decompose_lam_assum sigma c)))) with | Var id when Id.List.mem id (Tacmach.New.pf_ids_of_hyps gl) -> (* Like assert (id:=id args) but with the concept of specialization *) - let naming,tac = - prepare_intros_opt false (IntroIdentifier id) MoveLast ipat in + let naming,tac = prepare_intros_opt false (IntroIdentifier id) MoveLast ipat in let repl = do_replace (Some id) naming in Tacticals.New.tclTHENFIRST (assert_before_then_gen repl naming typ tac) @@ -3065,10 +3069,10 @@ let specialize (c,lbind) ipat = (* TODO: add intro to be more homogeneous. It will break scripts but will be easy to fix *) (Tacticals.New.tclTHENLAST (cut typ) (exact_no_check term)) - | Some {CAst.loc;v=ipat} -> + | Some _ as ipat -> (* Like pose proof with extra support for "with" bindings *) (* even though the "with" bindings forces full application *) - let naming,tac = prepare_intros ?loc false IntroAnonymous MoveLast ipat in + let naming, tac = prepare_intros_opt false IntroAnonymous MoveLast ipat in Tacticals.New.tclTHENFIRST (assert_before_then_gen false naming typ tac) (exact_no_check term) -- cgit v1.2.3 From 53e287871e2d03f95e754ffa58047668799e54ee Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 29 Nov 2020 02:10:56 +0100 Subject: Further simplifications in intro_patterns machinery. --- tactics/tactics.ml | 46 +++++++--------------------------------------- 1 file changed, 7 insertions(+), 39 deletions(-) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 09627b15c4..af46c06294 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2365,19 +2365,6 @@ let rec check_name_unicity env ok seen = let open CAst in function let wild_id = Id.of_string "_tmp" -let rec list_mem_assoc_right id = function - | [] -> false - | {CAst.v=id'}::l -> Id.equal id id' || list_mem_assoc_right id l - -let check_thin_clash_then id thin avoid tac = - if list_mem_assoc_right id thin then - let newid = next_ident_away (add_suffix id "'") avoid in - let thin = - List.map CAst.(map (fun id' -> if Id.equal id id' then newid else id')) thin in - Tacticals.New.tclTHEN (rename_hyp [id,newid]) (tac thin) - else - tac thin - let make_naming ?loc avoid l = function | IntroIdentifier id -> NamingMustBe (CAst.make ?loc id) | IntroAnonymous -> NamingAvoid (Id.Set.union avoid (explicit_intro_names l)) @@ -2386,10 +2373,8 @@ let make_naming ?loc avoid l = function 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 - IntroAnonymous, but at the cost of a "renaming"; Note that in the - case of IntroFresh, we should use check_thin_clash_then anyway to - prevent the case of an IntroFresh precisely using the wild_id *) + (* TODO: avoid wild_id to interfere with IntroFresh precisely using + the wild_id *) | IntroWildcard -> NamingBasedOn (wild_id, Id.Set.union avoid (explicit_intro_names l)) | IntroApplyOn (_,{CAst.v=pat;loc}) -> make_naming_pattern avoid ?loc l pat | (IntroOrAndPattern _ | IntroInjection _ | IntroRewrite _) as pat -> @@ -2439,38 +2424,21 @@ let rec intro_patterns_core with_evars avoid ids thin destopt bound n tac = [CAst.make @@ IntroNaming IntroAnonymous] | {CAst.loc;v=pat} :: l -> if exceed_bound n bound then error_unexpected_extra_pattern loc bound pat else + let naming = make_naming_pattern avoid l pat in match pat with | IntroForthcoming onlydeps -> - intro_forthcoming_then_gen (NamingAvoid (Id.Set.union avoid (explicit_intro_names l))) - destopt onlydeps bound n + intro_forthcoming_then_gen naming destopt onlydeps bound n (fun ids -> intro_patterns_core with_evars avoid ids thin destopt bound (n+List.length ids) tac l) | IntroAction pat -> - intro_then_gen (make_naming_action avoid l pat) - destopt true false + intro_then_gen naming 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 (fun ids thin -> intro_patterns_core with_evars avoid ids thin destopt bound (n+1) tac l))) | IntroNaming pat -> - intro_pattern_naming loc with_evars avoid ids pat thin destopt bound (n+1) tac l - - (* Pi-introduction rule, used backwards *) -and intro_pattern_naming loc with_evars avoid ids pat thin destopt bound n tac l = - match pat with - | IntroIdentifier id -> - check_thin_clash_then id thin avoid (fun thin -> - intro_then_gen (NamingMustBe CAst.(make ?loc id)) destopt true false - (fun id -> intro_patterns_core with_evars avoid (id::ids) thin destopt bound n tac l)) - | IntroAnonymous -> - intro_then_gen (NamingAvoid (Id.Set.union avoid (explicit_intro_names l))) - destopt true false - (fun id -> intro_patterns_core with_evars avoid (id::ids) thin destopt bound n tac l) - | IntroFresh id -> - (* todo: avoid thinned names to interfere with generation of fresh name *) - intro_then_gen (NamingBasedOn (id, Id.Set.union avoid (explicit_intro_names l))) - destopt true false - (fun id -> intro_patterns_core with_evars avoid (id::ids) thin destopt bound n tac l) + intro_then_gen naming destopt true false + (fun id -> intro_patterns_core with_evars avoid (id::ids) thin destopt bound (n+1) tac l) and intro_pattern_action ?loc with_evars pat thin destopt tac id = match pat with -- cgit v1.2.3 From eb38680520811e7a5e64678719d7b57e87af1269 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 29 Nov 2020 09:40:11 +0100 Subject: Preventing internal temporary names to impact the "?H"-like intro-pattern names. --- tactics/tactics.ml | 42 ++++++++++++++++++++++++++++-------------- test-suite/success/intros.v | 12 ++++++++++++ 2 files changed, 40 insertions(+), 14 deletions(-) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index af46c06294..f72764945c 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2324,21 +2324,31 @@ let rewrite_hyp_then with_evars thin l2r id tac = tclEVARSTHEN sigma (Tacticals.New.tclTHENFIRST eqtac (tac thin)) end -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) +let rec collect_intro_names = let open CAst in function +| {v=IntroForthcoming _} :: l -> collect_intro_names l +| {v=IntroNaming (IntroIdentifier id)} :: l -> + let ids1, ids2 = collect_intro_names l in Id.Set.add id ids1, ids2 | {v=IntroAction (IntroOrAndPattern l)} :: l' -> let ll = match l with IntroAndPattern l -> [l] | IntroOrPattern ll -> ll in - let fold accu l = Id.Set.union accu (explicit_intro_names (l@l')) in - List.fold_left fold Id.Set.empty ll + let fold (ids1',ids2') l = + let ids1, ids2 = collect_intro_names (l@l') in + Id.Set.union ids1 ids1', Id.Set.union ids2 ids2' in + List.fold_left fold (Id.Set.empty,Id.Set.empty) ll | {v=IntroAction (IntroInjection l)} :: l' -> - explicit_intro_names (l@l') + collect_intro_names (l@l') | {v=IntroAction (IntroApplyOn (c,pat))} :: l' -> - explicit_intro_names (pat::l') -| {v=(IntroNaming (IntroAnonymous | IntroFresh _) + collect_intro_names (pat::l') +| {v=IntroNaming (IntroFresh id)} :: l -> + let ids1, ids2 = collect_intro_names l in ids1, Id.Set.add id ids2 +| {v=(IntroNaming IntroAnonymous | IntroAction (IntroWildcard | IntroRewrite _))} :: l -> - explicit_intro_names l -| [] -> Id.Set.empty + collect_intro_names l +| [] -> Id.Set.empty, Id.Set.empty + +let explicit_intro_names l = fst (collect_intro_names l) + +let explicit_all_intro_names l = + let ids1,ids2 = collect_intro_names l in Id.Set.union ids1 ids2 let rec check_name_unicity env ok seen = let open CAst in function | {v=IntroForthcoming _} :: l -> check_name_unicity env ok seen l @@ -2363,7 +2373,12 @@ let rec check_name_unicity env ok seen = let open CAst in function check_name_unicity env ok seen l | [] -> () -let wild_id = Id.of_string "_tmp" +let fresh_wild ids = + let rec aux s = + if Id.Set.exists (fun id -> String.is_prefix s (Id.to_string id)) ids + then aux (s ^ "'") + else Id.of_string s in + aux "_H" let make_naming ?loc avoid l = function | IntroIdentifier id -> NamingMustBe (CAst.make ?loc id) @@ -2373,9 +2388,8 @@ let make_naming ?loc avoid l = function 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 *) - (* TODO: avoid wild_id to interfere with IntroFresh precisely using - the wild_id *) - | IntroWildcard -> NamingBasedOn (wild_id, Id.Set.union avoid (explicit_intro_names l)) + | IntroWildcard -> + NamingBasedOn (fresh_wild (Id.Set.union avoid (explicit_all_intro_names l)), Id.Set.empty) | 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))) diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index d37ad9f528..b8fbff05c6 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -152,3 +152,15 @@ Definition d := ltac:(intro x; exact (x*x)). Definition d' : nat -> _ := ltac:(intros;exact 0). End Evar. + +Module Wildcard. + +(* We check that the wildcard internal name does not interfere with + user fresh names (currently the prefix is "_H") *) + +Goal nat -> bool -> nat -> bool. +intros _ ?_H ?_H. +exact _H. +Qed. + +End Wildcard. -- cgit v1.2.3 From 660e3d01d0c73933a4595e2e8da92b00551a82ae Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 30 Nov 2020 13:06:43 +0100 Subject: Adding overlay for perennial. --- ...12-herbelin-master+fix13413-apply-on-intro-pattern-fresh-names.sh | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 dev/ci/user-overlays/13512-herbelin-master+fix13413-apply-on-intro-pattern-fresh-names.sh diff --git a/dev/ci/user-overlays/13512-herbelin-master+fix13413-apply-on-intro-pattern-fresh-names.sh b/dev/ci/user-overlays/13512-herbelin-master+fix13413-apply-on-intro-pattern-fresh-names.sh new file mode 100644 index 0000000000..4c8cdbbb45 --- /dev/null +++ b/dev/ci/user-overlays/13512-herbelin-master+fix13413-apply-on-intro-pattern-fresh-names.sh @@ -0,0 +1,5 @@ +if [ "$CI_PULL_REQUEST" = "13415" ] || [ "$CI_BRANCH" = "intern-univs" ]; then + + overlay perennial https://github.com/herbelin/perennial master+adapt13512-fresness-names-apply-in-introduction-pattern + +fi -- cgit v1.2.3 From 3878333deb3294cc54b1d9ce4599f71613ae9e3d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 2 Dec 2020 22:04:39 +0100 Subject: Adding changelog for #13512. --- .../13512-master+fix13413-apply-on-intro-pattern-fresh-names.rst | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 doc/changelog/04-tactics/13512-master+fix13413-apply-on-intro-pattern-fresh-names.rst diff --git a/doc/changelog/04-tactics/13512-master+fix13413-apply-on-intro-pattern-fresh-names.rst b/doc/changelog/04-tactics/13512-master+fix13413-apply-on-intro-pattern-fresh-names.rst new file mode 100644 index 0000000000..aaacb2aadf --- /dev/null +++ b/doc/changelog/04-tactics/13512-master+fix13413-apply-on-intro-pattern-fresh-names.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Possible collision between a user-level name and an internal name when + using the :n:`%` introduction pattern + (`#13512 `_, + fixes `#13413 `_, + by Hugo Herbelin). -- cgit v1.2.3