Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix list deprecations #21

Merged
merged 2 commits into from
Oct 15, 2023
Merged

Fix list deprecations #21

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
30506da
fix list deprecations
palmskog Oct 15, 2023
8ddc59f
refresh boilerplate
palmskog Oct 15, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .github/workflows/docker-action.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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'
Expand Down
2 changes: 1 addition & 1 deletion core/Combinators.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
12 changes: 7 additions & 5 deletions core/Tactics.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
8 changes: 4 additions & 4 deletions core/Tree.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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).
Expand Down Expand Up @@ -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;
Expand All @@ -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;
Expand Down
1 change: 1 addition & 0 deletions meta.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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'
Expand Down