diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 4 | ||||
| -rw-r--r-- | tactics/tactics.mli | 1 |
2 files changed, 5 insertions, 0 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5fe87a94c5..315c42097d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2265,6 +2265,10 @@ let left_with_bindings with_evars = constructor_tac with_evars (Some 2) 1 let right_with_bindings with_evars = constructor_tac with_evars (Some 2) 2 let split_with_bindings with_evars l = Tacticals.New.tclMAP (constructor_tac with_evars (Some 1) 1) l +let split_with_delayed_bindings with_evars = + Tacticals.New.tclMAP (fun bl -> + Tacticals.New.tclDELAYEDWITHHOLES with_evars bl + (constructor_tac with_evars (Some 1) 1)) let left = left_with_bindings false let simplest_left = left NoBindings diff --git a/tactics/tactics.mli b/tactics/tactics.mli index b6eb48a3d9..5b397b15d0 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -337,6 +337,7 @@ val split : constr bindings -> unit Proofview.tactic val left_with_bindings : evars_flag -> constr bindings -> unit Proofview.tactic val right_with_bindings : evars_flag -> constr bindings -> unit Proofview.tactic val split_with_bindings : evars_flag -> constr bindings list -> unit Proofview.tactic +val split_with_delayed_bindings : evars_flag -> constr bindings delayed_open list -> unit Proofview.tactic val simplest_left : unit Proofview.tactic val simplest_right : unit Proofview.tactic |