Merge PR #13468: Fixes #13456: regression in tactic exists which star…

…ted to check resolution of evars more incrementally

Ack-by: SkySkimmer
Reviewed-by: gares
Ack-by: ppedrot

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

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

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

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.