From 85d7906cb22d66debaf68d0e5713336deb724305 Mon Sep 17 00:00:00 2001
From: Attila Gáspár
Date: Tue, 19 May 2020 19:12:03 +0200
Subject: Delay evaluating arguments of the "exists" tactic

---
 tactics/tactics.ml  | 4 ++++
 tactics/tactics.mli | 1 +
 2 files changed, 5 insertions(+)

(limited to 'tactics')

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
-- 
cgit v1.2.3