aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/04-tactics/13761-remove_convert_concl_nc.rst4
-rw-r--r--doc/changelog/04-tactics/13762-remove_double_induction.rst9
-rw-r--r--doc/sphinx/changes.rst2
-rw-r--r--doc/sphinx/proof-engine/tactics.rst27
-rw-r--r--doc/sphinx/proofs/writing-proofs/rewriting.rst12
-rw-r--r--plugins/ltac/coretactics.mlg7
-rw-r--r--plugins/ltac/g_auto.mlg15
-rw-r--r--tactics/elim.ml52
-rw-r--r--tactics/elim.mli1
-rw-r--r--tactics/tactics.ml3
-rw-r--r--tactics/tactics.mli9
-rw-r--r--test-suite/success/induct.v44
12 files changed, 28 insertions, 157 deletions
diff --git a/doc/changelog/04-tactics/13761-remove_convert_concl_nc.rst b/doc/changelog/04-tactics/13761-remove_convert_concl_nc.rst
new file mode 100644
index 0000000000..1aa57ff8b1
--- /dev/null
+++ b/doc/changelog/04-tactics/13761-remove_convert_concl_nc.rst
@@ -0,0 +1,4 @@
+- **Removed:**
+ convert_concl_no_check. Use :tacn:`change_no_check` instead
+ (`#13761 <https://github.com/coq/coq/pull/13761>`_,
+ by Jim Fehrle).
diff --git a/doc/changelog/04-tactics/13762-remove_double_induction.rst b/doc/changelog/04-tactics/13762-remove_double_induction.rst
new file mode 100644
index 0000000000..4ea54a1ab6
--- /dev/null
+++ b/doc/changelog/04-tactics/13762-remove_double_induction.rst
@@ -0,0 +1,9 @@
+- **Removed:**
+ double induction tactic. Replace :n:`double induction @ident @ident`
+ with :n:`induction @ident; induction @ident` (or
+ :n:`induction @ident ; destruct @ident` depending on the exact needs).
+ Replace :n:`double induction @natural__1 @natural__2` with
+ :n:`induction @natural__1; induction natural__3` where :n:`natural__3` is the result
+ of :n:`natural__2 - natural__1`
+ (`#13762 <https://github.com/coq/coq/pull/13762>`_,
+ by Jim Fehrle).
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 7db54987d6..a08a110930 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -3191,7 +3191,7 @@ Other changes in 8.10+beta1
by Maxime Dénès, review by Pierre-Marie Pédrot).
- New variant :tacn:`change_no_check` of :tacn:`change`, usable as a
- documented replacement of :tacn:`convert_concl_no_check`
+ documented replacement of `convert_concl_no_check`
(`#10012 <https://github.com/coq/coq/pull/10012>`_,
`#10017 <https://github.com/coq/coq/pull/10017>`_,
`#10053 <https://github.com/coq/coq/pull/10053>`_, and
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 766f7ab44e..72970f46b0 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -498,10 +498,16 @@ one or more of its hypotheses.
:n:`{? - } {+ @nat_or_var }`
Selects the specified occurrences within a single goal or hypothesis.
- Occurrences are numbered from left to right starting with 1 when the
- goal is printed with the :flag:`Printing All` flag. (In particular, occurrences
- in :ref:`implicit arguments <ImplicitArguments>` and
- :ref:`coercions <Coercions>` are counted but not shown by default.)
+ Occurrences are numbered starting with 1 following a depth-first traversal
+ of the term's expression, including occurrences in
+ :ref:`implicit arguments <ImplicitArguments>`
+ and :ref:`coercions <Coercions>` that are not displayed by default.
+ (Set the :flag:`Printing All` flag to show those in the printed term.)
+
+ For example, when matching the pattern `_ + _` in the term `(a + b) + c`,
+ occurrence 1 is `(...) + c` and
+ occurrence 2 is `(a + b)`. When matching that pattern with term `a + (b + c)`,
+ occurrence 1 is `a + (...)` and occurrence 2 is `b + c`.
Specifying `-` includes all occurrences *except* the ones listed.
@@ -2067,19 +2073,6 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
is the name given by :n:`intros until @natural` to the :n:`@natural`-th non-dependent
premise of the goal.
-.. tacn:: double induction @ident @ident
- :name: double induction
-
- This tactic is deprecated and should be replaced by
- :n:`induction @ident; induction @ident` (or
- :n:`induction @ident ; destruct @ident` depending on the exact needs).
-
-.. tacv:: double induction @natural__1 @natural__2
-
- This tactic is deprecated and should be replaced by
- :n:`induction num1; induction num3` where :n:`num3` is the result
- of :n:`num2 - num1`
-
.. tacn:: dependent induction @ident
:name: dependent induction
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst
index 8c8c88c526..663337bc64 100644
--- a/doc/sphinx/proofs/writing-proofs/rewriting.rst
+++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst
@@ -91,7 +91,10 @@ Rewriting with Leibniz and setoid equality
in the conclusion is replaced.
If :n:`at @occs_nums` is specified, rewriting is always done with
- :ref:`setoid rewriting <generalizedrewriting>`, even for Leibniz’s equality.
+ :ref:`setoid rewriting <generalizedrewriting>`, even for Leibniz’s equality,
+ which means that you must `Require Setoid` to use that form.
+ However, note that :tacn:`rewrite` (even when using setoid rewriting) and
+ :tacn:`setoid_rewrite` don't behave identically (as already mentioned above).
:n:`by @ltac_expr3`
If specified, is used to resolve all side conditions generated by the tactic.
@@ -338,13 +341,6 @@ Rewriting with definitional equality
exact H.
Qed.
- .. tacn:: convert_concl_no_check @one_term
-
- .. deprecated:: 8.11
-
- Deprecated old name for :tacn:`change_no_check`. Does not support any of its
- variants.
-
.. _performingcomputations:
Performing computations
diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg
index e39c066c95..b20c4d173d 100644
--- a/plugins/ltac/coretactics.mlg
+++ b/plugins/ltac/coretactics.mlg
@@ -259,13 +259,6 @@ TACTIC EXTEND simple_destruct
| [ "simple" "destruct" quantified_hypothesis(h) ] -> { simple_destruct h }
END
-(** Double induction *)
-
-TACTIC EXTEND double_induction DEPRECATED { Deprecation.make () }
-| [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] ->
- { Elim.h_double_induction h1 h2 }
-END
-
(* Admit *)
TACTIC EXTEND admit
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 069a342b2a..82b41e41bd 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -11,7 +11,6 @@
{
open Pp
-open Constr
open Stdarg
open Pcoq.Prim
open Pcoq.Constr
@@ -199,20 +198,6 @@ TACTIC EXTEND unify
END
{
-let deprecated_convert_concl_no_check =
- CWarnings.create
- ~name:"convert_concl_no_check" ~category:"deprecated"
- (fun () -> Pp.str "The syntax [convert_concl_no_check] is deprecated. Use [change_no_check] instead.")
-}
-
-TACTIC EXTEND convert_concl_no_check
-| ["convert_concl_no_check" constr(x) ] -> {
- deprecated_convert_concl_no_check ();
- Tactics.convert_concl ~check:false x DEFAULTcast
- }
-END
-
-{
let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_qualid
let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Printer.pr_global
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 9a55cabc86..9e7843b2bb 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -19,7 +19,6 @@ open Tacmach.New
open Tacticals.New
open Clenv
open Tactics
-open Proofview.Notations
type branch_args = {
branchnum : int; (* the branch number *)
@@ -28,8 +27,6 @@ type branch_args = {
true=assumption, false=let-in *)
branchnames : Tactypes.intro_patterns}
-module NamedDecl = Context.Named.Declaration
-
type elim_kind = Case of bool | Elim
(* Find the right elimination suffix corresponding to the sort of the goal *)
@@ -217,52 +214,3 @@ let h_decompose l c = decompose_these c l
let h_decompose_or = decompose_or
let h_decompose_and = decompose_and
-
-(* The tactic Double performs a double induction *)
-
-let induction_trailer abs_i abs_j bargs =
- tclTHEN
- (tclDO (abs_j - abs_i) intro)
- (onLastHypId
- (fun id ->
- Proofview.Goal.enter begin fun gl ->
- let idty = pf_get_type_of gl (mkVar id) in
- let fvty = global_vars (pf_env gl) (project gl) idty in
- let possible_bring_hyps =
- (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs
- in
- let (hyps,_) =
- List.fold_left
- (fun (bring_ids,leave_ids) d ->
- let cid = NamedDecl.get_id d in
- if not (List.mem cid leave_ids)
- then (d::bring_ids,leave_ids)
- else (bring_ids,cid::leave_ids))
- ([],fvty) possible_bring_hyps
- in
- let ids = List.rev (ids_of_named_context hyps) in
- (tclTHENLIST
- [revert ids; elimination_then (fun _ -> tclIDTAC) id])
- end
- ))
-
-let double_ind h1 h2 =
- Proofview.Goal.enter begin fun gl ->
- let abs_i = depth_of_quantified_hypothesis true h1 gl in
- let abs_j = depth_of_quantified_hypothesis true h2 gl in
- let abs =
- if abs_i < abs_j then Proofview.tclUNIT (abs_i,abs_j) else
- if abs_i > abs_j then Proofview.tclUNIT (abs_j,abs_i) else
- let info = Exninfo.reify () in
- tclZEROMSG ~info (Pp.str "Both hypotheses are the same.") in
- abs >>= fun (abs_i,abs_j) ->
- (tclTHEN (tclDO abs_i intro)
- (onLastHypId
- (fun id ->
- elimination_then
- (introElimAssumsThen (induction_trailer abs_i abs_j)) id)))
- end
-
-let h_double_induction = double_ind
-
-
diff --git a/tactics/elim.mli b/tactics/elim.mli
index 01053502e4..a603b472f7 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -21,4 +21,3 @@ val case_tac : bool -> or_and_intro_pattern option ->
val h_decompose : inductive list -> constr -> unit Proofview.tactic
val h_decompose_or : constr -> unit Proofview.tactic
val h_decompose_and : constr -> unit Proofview.tactic
-val h_double_induction : quantified_hypothesis -> quantified_hypothesis-> unit Proofview.tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c64f583428..cbf12ac22f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -156,9 +156,6 @@ let convert_hyp ~check ~reorder d =
end
end
-let convert_concl_no_check = convert_concl ~check:false
-let convert_hyp_no_check = convert_hyp ~check:false ~reorder:false
-
let convert_gen pb x y =
Proofview.Goal.enter begin fun gl ->
match Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y with
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index a6471be549..c07073a91a 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -35,10 +35,6 @@ val is_quantified_hypothesis : Id.t -> Proofview.Goal.t -> bool
val introduction : Id.t -> unit Proofview.tactic
val convert_concl : check:bool -> types -> cast_kind -> unit Proofview.tactic
val convert_hyp : check:bool -> reorder:bool -> named_declaration -> unit Proofview.tactic
-val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic
-[@@ocaml.deprecated "use [Tactics.convert_concl]"]
-val convert_hyp_no_check : named_declaration -> unit Proofview.tactic
-[@@ocaml.deprecated "use [Tactics.convert_hyp]"]
val mutual_fix :
Id.t -> int -> (Id.t * int * constr) list -> int -> unit Proofview.tactic
val fix : Id.t -> int -> unit Proofview.tactic
@@ -81,11 +77,6 @@ val auto_intros_tac : Names.Name.t list -> unit Proofview.tactic
val intros : unit Proofview.tactic
-(** [depth_of_quantified_hypothesis b h g] returns the index of [h] in
- the conclusion of goal [g], up to head-reduction if [b] is [true] *)
-val depth_of_quantified_hypothesis :
- bool -> quantified_hypothesis -> Proofview.Goal.t -> int
-
val intros_until : quantified_hypothesis -> unit Proofview.tactic
val intros_clearing : bool list -> unit Proofview.tactic
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index 4983ee3c0d..615350c58c 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -154,50 +154,6 @@ induction H.
change (0 = z -> True) in IHrepr''.
Abort.
-(* Test double induction *)
-
-(* This was failing in 8.5 and before because of a bug in the order of
- hypotheses *)
-
-Set Warnings "-deprecated".
-
-Inductive I2 : Type :=
- C2 : forall x:nat, x=x -> I2.
-Goal forall a b:I2, a = b.
-double induction a b.
-Abort.
-
-(* This was leaving useless hypotheses in 8.5 and before because of
- the same bug. This is a change of compatibility. *)
-
-Inductive I3 : Prop :=
- C3 : forall x:nat, x=x -> I3.
-Goal forall a b:I3, a = b.
-double induction a b.
-Fail clear H. (* H should have been erased *)
-Abort.
-
-(* This one had quantification in reverse order in 8.5 and before *)
-(* This is a change of compatibility. *)
-
-Goal forall m n, le m n -> le n m -> n=m.
-intros m n. double induction 1 2.
-3:destruct 1. (* Should be "S m0 <= m0" *)
-Abort.
-
-(* Idem *)
-
-Goal forall m n p q, le m n -> le p q -> n+p=m+q.
-intros *. double induction 1 2.
-3:clear H2. (* H2 should have been erased *)
-Abort.
-
-(* This is unchanged *)
-
-Goal forall m n:nat, n=m.
-double induction m n.
-Abort.
-
(* Mentioned as part of bug #12944 *)
Inductive test : Set := cons : forall (IHv : nat) (v : test), test.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 07:51:21 +0000