Adapt to coq/coq#19530

test/serlib/genarg/libTactics.v

@@ -44,7 +44,7 @@
 
 Set Implicit Arguments.
 
-Require Import Stdlib.Lists.List.
+Require Import Stdlib.Lists.ListDef.
 
 
 (* ********************************************************************** *)
@@ -55,7 +55,9 @@ Require Import Stdlib.Lists.List.
   Lemma test : forall b, b = false.
   time eauto 7. (* takes over 4 seconds  to fail! *) *)
 
+(* now requires Stdlib
 #[global] Remove Hints Bool.trans_eq_bool.
+*)
 
 
 (* ********************************************************************** *)
@@ -260,7 +262,7 @@ Notation "'>>' v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13" :=
 
 Ltac list_boxer_of E :=
   match type of E with
-  | List.list Boxer => constr:(E)
+  | list Boxer => constr:(E)
   | _ => constr:((boxer E)::nil)
   end.
 
@@ -370,19 +372,19 @@ Ltac fast_rm_inside E :=
     Note: the tactic [number_to_nat] is extended in [LibInt] to
     take into account the [int] type, alias for [Z]. *)
 
-Require Stdlib.Numbers.BinNums Stdlib.ZArith.BinInt.
+Require Stdlib.Numbers.BinNums Stdlib.BinNums.IntDef.
 
-Definition ltac_int_to_nat (x:BinInt.Z) : nat :=
+Definition ltac_int_to_nat (x:BinNums.Z) : nat :=
   match x with
-  | BinInt.Z0 => 0%nat
-  | BinInt.Zpos p => BinPos.nat_of_P p
-  | BinInt.Zneg p => 0%nat
+  | BinNums.Z0 => 0%nat
+  | BinNums.Zpos p => PosDef.Pos.to_nat p
+  | BinNums.Zneg p => 0%nat
   end.
 
 Ltac number_to_nat N :=
   match type of N with
   | nat => constr:(N)
-  | BinInt.Z => let N' := constr:(ltac_int_to_nat N) in eval compute in N'
+  | BinNums.Z => let N' := constr:(ltac_int_to_nat N) in eval compute in N'
   end.
 
 (** [ltac_pattern E at K] is the same as [pattern E at K] except that
@@ -1547,7 +1549,7 @@ Ltac equates_one n :=
 
 Ltac equates_several E cont :=
   let all_pos := match type of E with
-    | List.list Boxer => constr:(E)
+    | list Boxer => constr:(E)
     | _ => constr:((boxer E)::nil)
     end in
   let rec go pos :=
@@ -2103,7 +2105,7 @@ Tactic Notation "sets_eq_let" ident(X) "in" hyp(H) :=
 
 Ltac rewrites_base E cont :=
   match type of E with
-  | List.list Boxer => forwards_then E cont
+  | list Boxer => forwards_then E cont
   | _ => cont E; fast_rm_inside E
   end.
 
@@ -2229,11 +2231,13 @@ Tactic Notation "replaces" constr(E) "with" constr(F) "in" hyp(H) :=
     with [F] in the current goal. Syntax [replaces E at K with F in H]
     is also available. *)
 
+(*
 Tactic Notation "replaces" constr(E) "at" constr(K) "with" constr(F) :=
   let T := fresh "TEMP" in assert (T: E = F); [ | rewrites T at K; clear T ].
 
 Tactic Notation "replaces" constr(E) "at" constr(K) "with" constr(F) "in" hyp(H) :=
   let T := fresh "TEMP" in assert (T: E = F); [ | rewrites T at K in H; clear T ].
+*)
 
 
 (* ---------------------------------------------------------------------- *)
@@ -2519,6 +2523,7 @@ Tactic Notation "subst_eq" constr(E) :=
 (* ---------------------------------------------------------------------- *)
 (** ** Tactics to work with proof irrelevance *)
 
+(* now requires Stdlib
 Require Import Stdlib.Logic.ProofIrrelevance.
 
 (** [pi_rewrite E] replaces [E] of type [Prop] with a fresh
@@ -2535,6 +2540,7 @@ Tactic Notation "pi_rewrite" constr(E) :=
   pi_rewrite_base E ltac:(fun X => rewrite X).
 Tactic Notation "pi_rewrite" constr(E) "in" hyp(H) :=
   pi_rewrite_base E ltac:(fun X => rewrite X in H).
+*)
 
 
 (* ---------------------------------------------------------------------- *)
@@ -2564,6 +2570,7 @@ Tactic Notation "fequal" :=
     [fequals] applies to goals of the form [f x1 .. xN = f y1 .. yN]
     and produces some subgoals of the form [xi = yi]). *)
 
+(* now requires Stdlib
 Ltac fequal_post :=
   first [ reflexivity | congruence | apply proof_irrelevance | idtac ].
 
@@ -2575,6 +2582,7 @@ Tactic Notation "fequals" :=
 
 Tactic Notation "fequals_rec" :=
   repeat (progress fequals).
+*)
 
 
 
@@ -3098,13 +3106,16 @@ Tactic Notation "cases_if'" :=
     [inductions E gen X1 .. XN] is a shorthand for
     [dependent induction E generalizing X1 .. XN]. *)
 
+(* now requires Stdlib
 Require Import Stdlib.Program.Equality.
+*)
 
 Ltac inductions_post :=
   unfold eq' in *.
 
 Tactic Notation "inductions" ident(E) :=
   dependent induction E; inductions_post.
+(* now requires Stdlib
 Tactic Notation "inductions" ident(E) "gen" ident(X1) :=
   dependent induction E generalizing X1; inductions_post.
 Tactic Notation "inductions" ident(E) "gen" ident(X1) ident(X2) :=
@@ -3127,6 +3138,7 @@ Tactic Notation "inductions" ident(E) "gen" ident(X1) ident(X2)
 Tactic Notation "inductions" ident(E) "gen" ident(X1) ident(X2)
  ident(X3) ident(X4) ident(X5) ident(X6) ident(X7) ident(X8) :=
   dependent induction E generalizing X1 X2 X3 X4 X5 X6 X7 X8; inductions_post.
+*)
 
 (** [induction_wf IH: E X] is used to apply the well-founded induction
     principle, for a given well-founded relation. It applies to a goal
@@ -3189,6 +3201,7 @@ Tactic Notation "induction_wf" ":" constr(E) ident(X) :=
     judgment that includes a counter for the maximal height
     (see LibTacticsDemos for an example) *)
 
+(* now Requires Stdlib
 Require Import Stdlib.Arith.Compare_dec.
 Require Import Lia.
 
@@ -3211,6 +3224,7 @@ Ltac induct_height_step x :=
  end.
 
 Ltac induct_height := induct_height_step O.
+*)
 
 
 (* ********************************************************************** *)
@@ -4047,12 +4061,14 @@ Tactic Notation "erewrite" "~" constr(E) :=
 
 Tactic Notation "fequal" "~" :=
   fequal; auto_tilde.
+(*
 Tactic Notation "fequals" "~" :=
   fequals; auto_tilde.
 Tactic Notation "pi_rewrite" "~" constr(E) :=
   pi_rewrite E; auto_tilde.
 Tactic Notation "pi_rewrite" "~" constr(E) "in" hyp(H) :=
   pi_rewrite E in H; auto_tilde.
+*)
 
 Tactic Notation "invert" "~" hyp(H) :=
   invert H; auto_tilde.
@@ -4443,12 +4459,14 @@ Tactic Notation "erewrite" "*" constr(E) :=
 
 Tactic Notation "fequal" "*" :=
   fequal; auto_star.
+(*
 Tactic Notation "fequals" "*" :=
   fequals; auto_star.
 Tactic Notation "pi_rewrite" "*" constr(E) :=
   pi_rewrite E; auto_star.
 Tactic Notation "pi_rewrite" "*" constr(E) "in" hyp(H) :=
   pi_rewrite E in H; auto_star.
+*)
 
 Tactic Notation "invert" "*" hyp(H) :=
   invert H; auto_star.