Merge pull request #96 from Villetaneuse/rm_arith_files

adapt to coq/coq#18164
mit-plv · Nov 29, 2023 · 90a9655 · 90a9655
2 parents 705bde5 + 9046608
commit 90a9655
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.