From 17f68d403d248e899efbb76afeed169232946ecf Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 17 Sep 2014 16:20:50 +0200 Subject: Fix bug #3633 properly, by delaying the interpetation of constrs in apply f, g,... so that apply f, g. succeeds when apply f; apply g does. It just mimicks the behavior of rewrite foo bar. --- tactics/tactics.mli | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'tactics/tactics.mli') diff --git a/tactics/tactics.mli b/tactics/tactics.mli index c076efb1f..398a90ba3 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -188,6 +188,9 @@ val eapply : constr -> unit Proofview.tactic val apply_with_bindings_gen : advanced_flag -> evars_flag -> (clear_flag * constr with_bindings located) list -> unit Proofview.tactic +val apply_with_delayed_bindings_gen : + advanced_flag -> evars_flag -> (clear_flag * delayed_open_constr_with_bindings located) list -> unit Proofview.tactic + val apply_with_bindings : constr with_bindings -> unit Proofview.tactic val eapply_with_bindings : constr with_bindings -> unit Proofview.tactic @@ -198,6 +201,11 @@ val apply_in : (clear_flag * constr with_bindings located) list -> intro_pattern option -> unit Proofview.tactic +val apply_delayed_in : + advanced_flag -> evars_flag -> clear_flag -> Id.t -> + (clear_flag * delayed_open_constr_with_bindings located) list -> + intro_pattern option -> unit Proofview.tactic + (** {6 Elimination tactics. } *) (* -- cgit v1.2.3