9 files changed, 3 insertions, 45 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 *)
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index b4527694ae..2e72ceae5a 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -114,11 +114,6 @@ END
 
 (** Eauto *)
 
-TACTIC EXTEND prolog DEPRECATED { Deprecation.make ~note:"Use eauto instead" () }
-| [ "prolog" "[" uconstr_list(l) "]" int_or_var(n) ] ->
-    { Eauto.prolog_tac (eval_uconstrs ist l) n }
-END
-
 {
 
 let make_depth n = snd (Eauto.make_dimension n None)
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 0e661543db..996f6b3eb3 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -173,8 +173,7 @@ GRAMMAR EXTEND Gram
           { TacFun (it,body) }
       | "let"; isrec = [IDENT "rec" -> { true } | -> { false } ];
           llc = LIST1 let_clause SEP "with"; "in";
-          body = tactic_expr LEVEL "5" -> { TacLetIn (isrec,llc,body) }
-      | IDENT "info"; tc = tactic_expr LEVEL "5" -> { TacInfo tc } ] ]
+          body = tactic_expr LEVEL "5" -> { TacLetIn (isrec,llc,body) } ] ]
   ;
   (* Tactic arguments to the right of an application *)
   tactic_arg_compat:
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index d74e981c6d..6233807016 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -642,7 +642,6 @@ let pr_goal_selector ~toplevel s =
   let lcall = 1
   let leval = 1
   let ltatom = 1
-  let linfo = 5
 
   let level_of p = match p with LevelLe n -> n | LevelLt n -> n-1 | LevelSome -> lseq
 
@@ -988,11 +987,6 @@ let pr_goal_selector ~toplevel s =
                 keyword "infoH" ++ spc ()
                 ++ pr_tac (LevelLe ltactical) t),
               ltactical
-            | TacInfo t ->
-              hov 1 (
-                keyword "info" ++ spc ()
-                ++ pr_tac (LevelLe ltactical) t),
-              linfo
             | TacOr (t1,t2) ->
               hov 1 (
                 pr_tac (LevelLt lorelse) t1 ++ spc ()
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index b77fb3acc7..b261096b63 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -225,7 +225,6 @@ and 'a gen_tactic_expr =
       'a gen_tactic_expr * Id.t option
   | TacId of 'n message_token list
   | TacFail of global_flag * int or_var * 'n message_token list
-  | TacInfo of 'a gen_tactic_expr
   | TacLetIn of rec_flag *
       (lname * 'a gen_tactic_arg) list *
       'a gen_tactic_expr
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index cfa224319c..650349b586 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -224,7 +224,6 @@ and 'a gen_tactic_expr =
       'a gen_tactic_expr * Id.t option
   | TacId of 'n message_token list
   | TacFail of global_flag * int or_var * 'n message_token list
-  | TacInfo of 'a gen_tactic_expr
   | TacLetIn of rec_flag *
       (lname * 'a gen_tactic_arg) list *
       'a gen_tactic_expr
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index bcfdb5318e..afa79a88db 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -649,7 +649,6 @@ and intern_tactic_seq onlytac ist = function
   | TacDo (n,tac) ->
       ist.ltacvars, TacDo (intern_int_or_var ist n,intern_pure_tactic ist tac)
   | TacTry tac -> ist.ltacvars, TacTry (intern_pure_tactic ist tac)
-  | TacInfo tac -> ist.ltacvars, TacInfo (intern_pure_tactic ist tac)
   | TacRepeat tac -> ist.ltacvars, TacRepeat (intern_pure_tactic ist tac)
   | TacTimeout (n,tac) ->
       ist.ltacvars, TacTimeout (intern_int_or_var ist n,intern_tactic onlytac ist tac)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 97f7a198e6..705a1a62ce 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1035,13 +1035,6 @@ let type_uconstr ?(flags = (constr_flags ()))
   understand_ltac flags env sigma vars expected_type term
   end
 
-let warn_deprecated_info =
-  CWarnings.create ~name:"deprecated-info-tactical" ~category:"deprecated"
-         (fun () ->
-          strbrk "The general \"info\" tactic is currently not working." ++ spc()++
-            strbrk "There is an \"Info\" command to replace it." ++fnl () ++
-            strbrk "Some specific verbose tactics may also exist, such as info_eauto.")
-
 (* Interprets an l-tac expression into a value *)
 let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftactic.t =
   (* The name [appl] of applied top-level Ltac names is ignored in
@@ -1154,9 +1147,6 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
   | TacSolve l -> Tacticals.New.tclSOLVE (List.map (interp_tactic ist) l)
   | TacComplete tac -> Tacticals.New.tclCOMPLETE (interp_tactic ist tac)
   | TacArg a -> interp_tactic ist (TacArg a)
-  | TacInfo tac ->
-      warn_deprecated_info ();
-      eval_tactic ist tac
   | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac)
   (* For extensions *)
   | TacAlias {loc; v=(s,l)} ->
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index ed298b7e66..c2f1589b74 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -200,7 +200,6 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
   | TacTimeout (n,tac) -> TacTimeout (n,subst_tactic subst tac)
   | TacTime (s,tac) -> TacTime (s,subst_tactic subst tac)
   | TacTry tac -> TacTry (subst_tactic subst tac)
-  | TacInfo tac -> TacInfo (subst_tactic subst tac)
   | TacRepeat tac -> TacRepeat (subst_tactic subst tac)
   | TacOr (tac1,tac2) ->
       TacOr (subst_tactic subst tac1,subst_tactic subst tac2)