Remove info tactic, deprecated in 8.5

7 files changed, 1 insertions, 22 deletions

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)