diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/coretactics.mlg | 20 |
1 files changed, 2 insertions, 18 deletions
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 *) |