Skip to content

Adapt to https://github.com/rocq-prover/rocq/pull/21478 #283

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

Open
proux01 wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Adapt to https://github.com/rocq-prover/rocq/pull/21478 #283

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
6 changes: 3 additions & 3 deletions secure_example/LabelledAsmCombinators.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -86,10 +86,10 @@ Definition app_bks {A B C D : nat} (ab : bks A B) (cd : bks C D)
end.

(** Simple combinator to build a [block] from its instructions and branch operation. *)
Fixpoint after {A: Type} (is : list instr) (bch : branch A) : block A :=
match is with
Fixpoint after {A: Type} (si : list instr) (bch : branch A) : block A :=
match si with
| nil => bbb bch
| i :: is => bbi i (after is bch)
| i :: si => bbi i (after si bch)
end.

(* SAZ: rationalize the names of the combinators? *)
Expand Down
14 changes: 7 additions & 7 deletions theories/Basics/Basics.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,10 @@
(** Not specific to itrees. *)

(* begin hide *)
From Coq Require

Check warning on line 6 in theories/Basics/Basics.v

View workflow job for this annotation

GitHub Actions / build (rocq/rocq-prover:9.0) 

"From Coq" has been replaced by "From Stdlib".

Check warning on line 6 in theories/Basics/Basics.v

View workflow job for this annotation

GitHub Actions / build (rocq/rocq-prover:dev) 

"From Coq" has been replaced by "From Stdlib".
Ensembles.

From Coq Require Import

Check warning on line 9 in theories/Basics/Basics.v

View workflow job for this annotation

GitHub Actions / build (rocq/rocq-prover:9.0) 

"From Coq" has been replaced by "From Stdlib".

Check warning on line 9 in theories/Basics/Basics.v

View workflow job for this annotation

GitHub Actions / build (rocq/rocq-prover:dev) 

"From Coq" has been replaced by "From Stdlib".
RelationClasses.

From ExtLib Require Import
Expand Down Expand Up @@ -43,7 +43,7 @@
Definition idM {E : Type -> Type} : E ~> E := fun _ e => e.

(** [void] is a shorthand for [Empty_set]. *)
Notation void := Empty_set.

Check warning on line 46 in theories/Basics/Basics.v

View workflow job for this annotation

GitHub Actions / build (rocq/rocq-prover:dev) 

Use of "Notation" keyword for abbreviations is deprecated, use

(** ** Common monads and transformers. *)

Expand Down Expand Up @@ -104,13 +104,13 @@
#[global] Instance MonadIter_stateT {M S} {MM : Monad M} {AM : MonadIter M}
: MonadIter (stateT S M) :=
fun _ _ step i => mkStateT (fun s =>
iter (fun is =>
let i := fst is in
let s := snd is in
is' <- runStateT (step i) s ;;
ret match fst is' with
| inl i' => inl (i', snd is')
| inr r => inr (r, snd is')
iter (fun si =>
let i := fst si in
let s := snd si in
si' <- runStateT (step i) s ;;
ret match fst si' with
| inl i' => inl (i', snd si')
| inr r => inr (r, snd si')
end) (i, s)).

#[global] Polymorphic Instance MonadIter_stateT0 {M S} {MM : Monad M} {AM : MonadIter M}
Expand Down
6 changes: 3 additions & 3 deletions tutorial/AsmCombinators.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -79,10 +79,10 @@ Definition app_bks {A B C D : nat} (ab : bks A B) (cd : bks C D)
end.

(** Simple combinator to build a [block] from its instructions and branch operation. *)
Fixpoint after {A: Type} (is : list instr) (bch : branch A) : block A :=
match is with
Fixpoint after {A: Type} (si : list instr) (bch : branch A) : block A :=
match si with
| nil => bbb bch
| i :: is => bbi i (after is bch)
| i :: si => bbi i (after si bch)
end.

(* SAZ: rationalize the names of the combinators? *)
Expand Down
Loading