diff options
| author | Gaëtan Gilbert | 2020-08-24 13:11:20 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-08-25 16:15:17 +0200 |
| commit | 2eac36b65732e0302f04693a4524c454fcbb5760 (patch) | |
| tree | 42fb4dbed70d041ec9fa0913a5a8f4ac0a366385 /plugins/funind/recdef.ml | |
| parent | 5e4d696c0a5c864092f7263b9bb7f7eb419d121e (diff) | |
funind: stop using intro_using
Diffstat (limited to 'plugins/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 253c95fa67..066ade07d2 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -414,7 +414,8 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = observe_tclTHENLIST (fun _ _ -> str "treat_case1") [ h_intros (List.rev rev_ids) - ; Proofview.V82.of_tactic (intro_using teq_id) + ; Proofview.V82.of_tactic + (intro_using_then teq_id (fun _ -> Proofview.tclUNIT ())) ; onLastHypId (fun heq -> observe_tclTHENLIST (fun _ _ -> str "treat_case2") @@ -601,7 +602,11 @@ let rec destruct_bounds_aux infos (bound, hyple, rechyps) lbounds g = (Proofview.V82.of_tactic (simplest_case (mkVar id))) [ observe_tclTHENLIST (fun _ _ -> str "") - [ Proofview.V82.of_tactic (intro_using h_id) + [ Proofview.V82.of_tactic + (intro_using_then h_id + (* We don't care about the refreshed name, + accessed only through auto? *) + (fun _ -> Proofview.tclUNIT ())) ; Proofview.V82.of_tactic (simplest_elim (mkApp (delayed_force lt_n_O, [|s_max|]))) @@ -865,7 +870,10 @@ let terminate_app_rec (f, args) expr_info continuation_tac _ g = (simplest_elim (mkApp (mkVar expr_info.ih, Array.of_list args)))) [ observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec2") - [ Proofview.V82.of_tactic (intro_using rec_res_id) + [ Proofview.V82.of_tactic + (intro_using_then rec_res_id + (* refreshed name gotten from onNthHypId *) + (fun _ -> Proofview.tclUNIT ())) ; Proofview.V82.of_tactic intro ; onNthHypId 1 (fun v_bound -> onNthHypId 2 (fun v -> |