diff options
| author | Pierre-Marie Pédrot | 2020-05-25 19:25:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-25 19:25:58 +0200 |
| commit | 8b3ce7442dcbcdf3d6b43efd0360ead334819913 (patch) | |
| tree | 9beac631f4318c19b85f863e6763be0d771e9674 /tactics | |
| parent | 2100a8b5d8de37b45ba35028f2d66cedf9c8ad77 (diff) | |
| parent | 85d7906cb22d66debaf68d0e5713336deb724305 (diff) | |
Merge PR #12366: Delay evaluating arguments of the "exists" tactic
Reviewed-by: ppedrot
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 |