Merge PR #12366: Delay evaluating arguments of the "exists" tactic

Reviewed-by: ppedrot

5 files changed, 22 insertions, 18 deletions

diff --git a/doc/changelog/04-tactics/12366-fix-exists.rst b/doc/changelog/04-tactics/12366-fix-exists.rst
new file mode 100644
index 0000000000..6d976ff562
--- /dev/null
+++ b/doc/changelog/04-tactics/12366-fix-exists.rst
@@ -0,0 +1,7 @@
+- **Changed:**
+  When using :tacn:`exists` or :tacn:`eexists` with multiple arguments,
+  the evaluation of arguments and applications of constructors are now interleaved.
+  This improves unification in some cases
+  (`#12366 <https://github.com/coq/coq/pull/12366>`_,
+  fixes `#12365 <https://github.com/coq/coq/issues/12365>`_,
+  by Attila Gáspár).
diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg
index 48b6abf441..cb226de586 100644
--- a/plugins/ltac/coretactics.mlg
+++ b/plugins/ltac/coretactics.mlg
@@ -165,18 +165,6 @@ END
 
 (** Split *)
 
-{
-
-let rec delayed_list = function
-| [] -> fun _ sigma -> (sigma, [])
-| x :: l ->
-  fun env sigma ->
-    let (sigma, x) = x env sigma in
-    let (sigma, l) = delayed_list l env sigma in
-    (sigma, x :: l)
-
-}
-
 TACTIC EXTEND split
 | [ "split" ] -> { Tactics.split_with_bindings false [NoBindings] }
 END
@@ -199,16 +187,12 @@ END
 
 TACTIC EXTEND exists
 | [ "exists" ] -> { Tactics.split_with_bindings false [NoBindings] }
-| [ "exists" ne_bindings_list_sep(bll, ",") ] -> {
-    Tacticals.New.tclDELAYEDWITHHOLES false (delayed_list bll) (fun bll -> Tactics.split_with_bindings false bll)
-  }
+| [ "exists" ne_bindings_list_sep(bll, ",") ] -> { Tactics.split_with_delayed_bindings false bll }
 END
 
 TACTIC EXTEND eexists
 | [ "eexists" ] -> { Tactics.split_with_bindings true [NoBindings] }
-| [ "eexists" ne_bindings_list_sep(bll, ",") ] -> {
-    Tacticals.New.tclDELAYEDWITHHOLES true (delayed_list bll) (fun bll -> Tactics.split_with_bindings true bll)
-  }
+| [ "eexists" ne_bindings_list_sep(bll, ",") ] -> { Tactics.split_with_delayed_bindings true bll }
 END
 
 (** Intro *)
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
diff --git a/test-suite/bugs/closed/bug_12365.v b/test-suite/bugs/closed/bug_12365.v
new file mode 100644
index 0000000000..a8e2bb459d
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12365.v
@@ -0,0 +1,8 @@
+Parameter a b : nat.
+Parameter p : a = b.
+
+Goal exists (_ : True) (_ : exists x, x = b), True.
+Proof.
+  exists I, (ex_intro _ a p).
+  exact I.
+Qed.