From 90466086e2e28f58911096837baa8857b2dd480f Mon Sep 17 00:00:00 2001 From: Pierre Rousselin <rousselin@math.univ-paris13.fr> Date: Wed, 29 Nov 2023 20:49:12 +0100 Subject: [PATCH] adapt to Coq/Coq#18164 --- src/Rupicola/Lib/Arrays.v | 2 +- src/Rupicola/Lib/ControlFlow/DownTo.v | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Rupicola/Lib/Arrays.v b/src/Rupicola/Lib/Arrays.v index 4912d8a6..5abf5f38 100644 --- a/src/Rupicola/Lib/Arrays.v +++ b/src/Rupicola/Lib/Arrays.v @@ -279,7 +279,7 @@ Section with_parameters. Proof. intros; rewrite Hput by lia. rewrite List.firstn_app. - rewrite List.firstn_firstn, Min.min_idempotent. + rewrite List.firstn_firstn, Nat.min_idempotent. rewrite List.firstn_length_le by lia. rewrite Nat.sub_diag; cbn [List.firstn]; rewrite app_nil_r. reflexivity. diff --git a/src/Rupicola/Lib/ControlFlow/DownTo.v b/src/Rupicola/Lib/ControlFlow/DownTo.v index cfe42416..f645e564 100644 --- a/src/Rupicola/Lib/ControlFlow/DownTo.v +++ b/src/Rupicola/Lib/ControlFlow/DownTo.v @@ -29,7 +29,8 @@ Section Gallina. Nat.iter n f a = downto' a i (i + n) (fun a _ => f a). Proof. unfold downto'. - setoid_rewrite skipn_seq_step; setoid_rewrite minus_plus. + setoid_rewrite skipn_seq_step. + setoid_rewrite (Nat.add_comm _ n); setoid_rewrite Nat.add_sub. simpl; induction n; simpl; intros. - reflexivity. - rewrite fold_left_app.