diff options
| author | Attila Gáspár | 2020-05-19 19:12:03 +0200 |
|---|---|---|
| committer | Attila Gáspár | 2020-05-19 22:22:51 +0200 |
| commit | 85d7906cb22d66debaf68d0e5713336deb724305 (patch) | |
| tree | 7a6d65513b74ed7094fd768a7f49dfee68daa1be /tactics | |
| parent | ed0f2f08e31ee4e645aa6e52970ddefc60f1f4f9 (diff) | |
Delay evaluating arguments of the "exists" tactic
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 |