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 --- doc/changelog/04-tactics/12366-fix-exists.rst | 7 +++++++ plugins/ltac/coretactics.mlg | 20 ++------------------ tactics/tactics.ml | 4 ++++ tactics/tactics.mli | 1 + test-suite/bugs/closed/bug_12365.v | 8 ++++++++ 5 files changed, 22 insertions(+), 18 deletions(-) create mode 100644 doc/changelog/04-tactics/12366-fix-exists.rst create mode 100644 test-suite/bugs/closed/bug_12365.v 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 `_, + fixes `#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. -- cgit v1.2.3