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.

4 files changed, 38 insertions, 4 deletions

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 24aa178ed2..68afd9a128 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -727,6 +727,32 @@ module New = struct
       let (loc,_) = evi.Evd.evar_source in
       Pretype_errors.error_unsolvable_implicit ?loc env sigma evk None
 
+  let tclMAPDELAYEDWITHHOLES accept_unresolved_holes l tac =
+    let rec aux = function
+      | [] -> tclUNIT ()
+      | x :: l ->
+        Proofview.Goal.enter begin fun gl ->
+          let env = Proofview.Goal.env gl in
+          let sigma_initial = Proofview.Goal.sigma gl in
+          let (sigma, x) = x env sigma_initial in
+          Proofview.Unsafe.tclEVARS sigma <*> tac x >>= fun () -> aux l >>= fun () ->
+          if accept_unresolved_holes then
+            tclUNIT ()
+          else
+            tclEVARMAP >>= fun sigma_final ->
+            try
+              let () = check_evars env sigma_final sigma sigma_initial in
+              tclUNIT ()
+            with e when CErrors.noncritical e ->
+              let e, info = Exninfo.capture e in
+              tclZERO ~info e
+          end in
+    aux l
+
+  (* The following is basically
+    tclMAPDELAYEDWITHHOLES accept_unresolved_holes [fun _ _ -> (sigma,())] (fun () -> tac)
+    but with value not necessarily in unit *)
+
   let tclWITHHOLES accept_unresolved_holes tac sigma =
     tclEVARMAP >>= fun sigma_initial ->
       if sigma == sigma_initial then tac
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index e97c5f3c1f..19d08dcc36 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -209,6 +209,10 @@ module New : sig
   val tclSELECT : Goal_select.t -> 'a tactic -> 'a tactic
   val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic
   val tclDELAYEDWITHHOLES : bool -> 'a delayed_open -> ('a -> unit tactic) -> unit tactic
+  val tclMAPDELAYEDWITHHOLES : bool -> 'a delayed_open list -> ('a -> unit tactic) -> unit tactic
+  (* in [tclMAPDELAYEDWITHHOLES with_evars l tac] the delayed
+     argument of [l] are evaluated in the possibly-updated
+     environment and updated sigma of each new successive goals *)
 
   val tclTIMEOUT : int -> unit tactic -> unit tactic
   val tclTIME : string option -> 'a tactic -> 'a tactic
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
diff --git a/test-suite/bugs/closed/bug_13456.v b/test-suite/bugs/closed/bug_13456.v
new file mode 100644
index 0000000000..b2e7fa7be5
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13456.v
@@ -0,0 +1,5 @@
+Lemma minbug (n : nat) (P : nat -> Prop) (pn : P n) : exists (m : nat) (p : P m), True.
+Proof.
+  exists _, pn.
+  exact I.
+Qed.