From 0fa7e871234656d261e908c6f753d22984b331ca Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 14 Sep 2024 22:11:17 +0200 Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/19530 --- test/serlib/genarg/libTactics.v | 38 ++++++++++++++++++++++++--------- 1 file changed, 28 insertions(+), 10 deletions(-) diff --git a/test/serlib/genarg/libTactics.v b/test/serlib/genarg/libTactics.v index 5f895f69e..5c7886d77 100644 --- a/test/serlib/genarg/libTactics.v +++ b/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.