Merge pull request #21 from uwplse/fix-deprec

Fix list deprecations
uwplse · Oct 15, 2023 · c0b3478 · c0b3478
2 parents bad8ad2 + 8ddc59f
commit c0b3478
Show file tree

Hide file tree

Showing 5 changed files with 14 additions and 10 deletions.
diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
@@ -18,6 +18,7 @@ jobs:
       matrix:
         image:
           - 'coqorg/coq:dev'
+          - 'coqorg/coq:8.18'
           - 'coqorg/coq:8.17'
           - 'coqorg/coq:8.16'
           - 'coqorg/coq:8.15'

diff --git a/core/Combinators.v b/core/Combinators.v
@@ -148,7 +148,7 @@ Section BasicCombinators.
       rewrite ByteListReader.bind_unwrap.
       rewrite ByteListReader.map_unwrap.
       rewrite IOStreamWriter.append_unwrap.
-      rewrite app_ass.
+      rewrite <- app_assoc.
       rewrite serialize_deserialize_id.
       rewrite ByteListReader.bind_unwrap.
       rewrite IHl.

diff --git a/core/Tactics.v b/core/Tactics.v
@@ -6,8 +6,10 @@ From Cheerios Require Import Types.
 Ltac cheerios_crush := intros; autorewrite with cheerios; auto.
 
 #[global]
-Hint Rewrite app_ass
-     IOStreamWriter.empty_unwrap IOStreamWriter.putByte_unwrap
-     IOStreamWriter.append_unwrap
-     ByteListReader.getByte_unwrap ByteListReader.bind_unwrap ByteListReader.ret_unwrap
-     ByteListReader.map_unwrap @ByteListReader.fold_unwrap : cheerios.
+Hint Rewrite <- app_assoc : cheerios.
+#[global]
+Hint Rewrite
+ IOStreamWriter.empty_unwrap IOStreamWriter.putByte_unwrap
+ IOStreamWriter.append_unwrap
+ ByteListReader.getByte_unwrap ByteListReader.bind_unwrap ByteListReader.ret_unwrap
+ ByteListReader.map_unwrap @ByteListReader.fold_unwrap : cheerios.
diff --git a/core/Tree.v b/core/Tree.v
@@ -269,7 +269,7 @@ Proof.
                         fill'_list (List.map (map f) l) (preorder_list l ++ bs) = Some (l, bs)); intros.
   - auto.
   - simpl.
-    rewrite app_ass. rewrite  IHt. rewrite IHt0. auto.
+    rewrite <- app_assoc. rewrite  IHt. rewrite IHt0. auto.
   - auto.
   - simpl.
     fold (@preorder_list B).
@@ -366,9 +366,9 @@ Section serializer.
                             ((rev (List.map shape l) ++ ts) :: acc)) bytes);
       intros;
       try (unfold serialize_list_tree_shape;
-           rewrite IOStreamWriter.append_unwrap, app_ass, IHt, IHt0;
+           rewrite IOStreamWriter.append_unwrap, <- app_assoc, IHt, IHt0;
            simpl;
-           now rewrite app_ass).
+           now rewrite <- app_assoc).
     (cheerios_crush; simpl; cheerios_crush; simpl).
     -  destruct acc;
          repeat (cheerios_crush;
@@ -381,7 +381,7 @@ Section serializer.
         IOStreamWriter.putByte_unwrap;
         simpl;
         fold serialize_list_tree_shape;
-        rewrite app_ass, IHt, ByteListReader.fold_unwrap,
+        rewrite <- app_assoc, IHt, ByteListReader.fold_unwrap,
         IOStreamWriter.putByte_unwrap;
         simpl;
         rewrite app_nil_r, rev'_spec, rev_involutive;

diff --git a/meta.yml b/meta.yml
@@ -45,6 +45,7 @@ supported_coq_versions:
 
 tested_coq_opam_versions:
 - version: dev
+- version: '8.18'
 - version: '8.17'
 - version: '8.16'
 - version: '8.15'