adapt to coq/coq#18164

mit-plv · Nov 29, 2023 · 9046608 · 9046608
1 parent 705bde5
commit 9046608
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git 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
@@ -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.