diff options
| author | Hugo Herbelin | 2020-11-24 19:08:53 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-26 15:52:18 +0100 |
| commit | e353fe431351bb1f41bc6a8c813bea980e8d247c (patch) | |
| tree | 234b537d73fca9d5993804e0e5fae633397427dd /tactics/tactics.ml | |
| parent | 90cb2b0daf54cbd72c5ac8e1ffe2007c8901ddba (diff) | |
Fixes #13456: regression where tactic exists started to check evars incrementally.
The regression was due to #12365. We fix it by postponing the evars
check after the calls to the underlying constructor tactic, while
retaining using information from the first instantiations to resolve
the latter instantiations.
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 8b38bc1b0a..5aa31092e9 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2282,10 +2282,9 @@ 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 split_with_delayed_bindings with_evars bl = + Tacticals.New.tclMAPDELAYEDWITHHOLES with_evars bl + (constructor_tac with_evars (Some 1) 1) let left = left_with_bindings false let simplest_left = left NoBindings |