Adapt to coq/coq#18164

adampetcher · Nov 1, 2023 · d9ef832 · d9ef832
1 parent 7e1773e
commit d9ef832
Show file tree

Hide file tree

Showing 25 changed files with 635 additions and 679 deletions.
diff --git a/src/FCF/Array.v b/src/FCF/Array.v
@@ -667,7 +667,7 @@ Theorem arrayLookup_allNats_eq :
   rewrite app_length in H.
   rewrite fst_split_app_eq in H.
   simpl in *.
-  rewrite plus_comm in H.
+  rewrite Nat.add_comm in H.
   simpl in *.
   eapply app_inj_tail in H.
   intuition.