diff options
| author | Pierre-Marie Pédrot | 2020-09-08 10:37:24 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-08 10:37:24 +0200 |
| commit | dde607ce50ddcf5f965d4ce222ca50f4d169a2f3 (patch) | |
| tree | 7f1eb9b6d5af851e776b0a6eb7594eb8b8910c00 /tactics | |
| parent | edb2cefe61d5f5b3230ab33842e61423ca02fbdb (diff) | |
| parent | e5890700b4574ee9207b2daf6ec95707b9290275 (diff) | |
Merge PR #12954: Fixes a freshness issue with destruct/induction (see comment in #12944).
Ack-by: RalfJung
Ack-by: jashug
Reviewed-by: ppedrot
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5f7e35d205..d33f3a5062 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3248,13 +3248,10 @@ let rec consume_pattern avoid na isdep gl = let open CAst in function | {loc;v=IntroForthcoming true}::names when not isdep -> consume_pattern avoid na isdep gl names | {loc;v=IntroForthcoming _}::names as fullpat -> - let avoid = Id.Set.union avoid (explicit_intro_names names) in (CAst.make ?loc @@ intropattern_of_name gl avoid na, fullpat) | {loc;v=IntroNaming IntroAnonymous}::names -> - let avoid = Id.Set.union avoid (explicit_intro_names names) in (CAst.make ?loc @@ intropattern_of_name gl avoid na, names) | {loc;v=IntroNaming (IntroFresh id')}::names -> - let avoid = Id.Set.union avoid (explicit_intro_names names) in (CAst.make ?loc @@ IntroNaming (IntroIdentifier (new_fresh_id avoid id' gl)), names) | pat::names -> (pat,names) @@ -3312,7 +3309,7 @@ let get_recarg_dest (recargdests,tophyp) = *) let induct_discharge with_evars dests avoid' tac (avoid,ra) names = - let avoid = Id.Set.union avoid avoid' in + let avoid = Id.Set.union avoid' (Id.Set.union avoid (explicit_intro_names names)) in let rec peel_tac ra dests names thin = match ra with | (RecArg,_,deprec,recvarname) :: @@ -3320,7 +3317,7 @@ let induct_discharge with_evars dests avoid' tac (avoid,ra) names = Proofview.Goal.enter begin fun gl -> let (recpat,names) = match names with | [{CAst.loc;v=IntroNaming (IntroIdentifier id)} as pat] -> - let id' = next_ident_away (add_prefix "IH" id) avoid in + let id' = new_fresh_id avoid (add_prefix "IH" id) gl in (pat, [CAst.make @@ IntroNaming (IntroIdentifier id')]) | _ -> consume_pattern avoid (Name recvarname) deprec gl names in let dest = get_recarg_dest dests in |