aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/04-tactics/12423-rm-info.rst2
-rw-r--r--plugins/ltac/g_ltac.mlg3
-rw-r--r--plugins/ltac/pptactic.ml6
-rw-r--r--plugins/ltac/tacexpr.ml1
-rw-r--r--plugins/ltac/tacexpr.mli1
-rw-r--r--plugins/ltac/tacintern.ml1
-rw-r--r--plugins/ltac/tacinterp.ml10
-rw-r--r--plugins/ltac/tacsubst.ml1
-rw-r--r--test-suite/modules/PO.v10
-rw-r--r--test-suite/output/auto.v2
10 files changed, 9 insertions, 28 deletions
diff --git a/doc/changelog/04-tactics/12423-rm-info.rst b/doc/changelog/04-tactics/12423-rm-info.rst
new file mode 100644
index 0000000000..bf20453e6b
--- /dev/null
+++ b/doc/changelog/04-tactics/12423-rm-info.rst
@@ -0,0 +1,2 @@
+- **Removed:** Removed info tactic that was deprecated in 8.5.
+ (`#12423 <https://github.com/coq/coq/pull/12423>`_, by Jim Fehrle).
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)
diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v
index 4c0ee1b5bd..767b3c1922 100644
--- a/test-suite/modules/PO.v
+++ b/test-suite/modules/PO.v
@@ -23,11 +23,11 @@ Module Pair (X: PO) (Y: PO) <: PO.
Hint Unfold le.
Lemma le_refl : forall p : T, le p p.
- info auto.
+ auto.
Qed.
Lemma le_trans : forall p1 p2 p3 : T, le p1 p2 -> le p2 p3 -> le p1 p3.
- unfold le; intuition; info eauto.
+ unfold le; intuition; eauto.
Qed.
Lemma le_antis : forall p1 p2 : T, le p1 p2 -> le p2 p1 -> p1 = p2.
@@ -39,9 +39,9 @@ Module Pair (X: PO) (Y: PO) <: PO.
enough (t0 = t2) as ->.
reflexivity.
- info auto.
+ auto.
- info auto.
+ auto.
Qed.
End Pair.
@@ -53,5 +53,5 @@ Require Nat.
Module NN := Pair Nat Nat.
Lemma zz_min : forall p : NN.T, NN.le (0, 0) p.
- info auto with arith.
+ auto with arith.
Qed.
diff --git a/test-suite/output/auto.v b/test-suite/output/auto.v
index 92917cdfc7..7b295dd1cb 100644
--- a/test-suite/output/auto.v
+++ b/test-suite/output/auto.v
@@ -1,4 +1,4 @@
-(* testing info/debug auto/eauto *)
+(* testing info_*/debug auto/eauto *)
Goal False \/ (True -> True).
info_auto.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:06:49 +0000