From 77e6eda6388aba117476f6c8445c4b61ebdbc33e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 27 Dec 2015 00:44:58 +0100 Subject: Tentative API fix for tactic arguments to be fed to tclWITHHOLES. The previous implementation was a source of evar leaks if misused, as it created values coming together with their current evar_map. This is dead wrong if the value is not used on the spot. To fix this, we rather return a ['a delayed_open] object. Two argument types were modified: bindings and constr_bindings. The open_constr argument should also be fixed, but it is more entangled and thus I leave it for another commit. --- tactics/extratactics.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics/extratactics.mli') diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli index 72c2679c0..1d2e497d5 100644 --- a/tactics/extratactics.mli +++ b/tactics/extratactics.mli @@ -11,4 +11,4 @@ val injHyp : Names.Id.t -> unit Proofview.tactic (* val refine_tac : Evd.open_constr -> unit Proofview.tactic *) -val onSomeWithHoles : ('a option -> unit Proofview.tactic) -> 'a Evd.sigma option -> unit Proofview.tactic +val onSomeWithHoles : ('a option -> unit Proofview.tactic) -> 'a Tacexpr.delayed_open option -> unit Proofview.tactic -- cgit v1.2.3