diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-17 16:20:50 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-17 17:57:08 +0200 |
| commit | 17f68d403d248e899efbb76afeed169232946ecf (patch) | |
| tree | 5eb60ef760ea388670612c4c0ece96a43e7dad87 /tactics/tactics.mli | |
| parent | cc6afad3bcfaa5b7fa57c8cd3035fe520c93afda (diff) | |
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.
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 8 |
1 files changed, 8 insertions, 0 deletions
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. } *) (* |