Skip to content
Snippets Groups Projects
Commit 58864e5b authored by Hai Dang's avatar Hai Dang
Browse files

Bump gpfsl

parent d61f7e25
Branches
No related tags found
No related merge requests found
Pipeline #45270 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
coq-lambda-rust.opam
+ 1
− 1
View file @ 58864e5b
...@@ -15,7 +15,7 @@ This branch uses a proper weak memory model. ...@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
""" """
depends: [ depends: [
"coq-gpfsl" { (= "dev.2021-03-07.0.6acef1f1") | (= "dev") } "coq-gpfsl" { (= "dev.2021-04-14.2.89510b36") | (= "dev") }
] ]
build: [make "-j%{jobs}%"] build: [make "-j%{jobs}%"]
......
theories/typing/lib/rwlock/rwlockwriteguard_code.v
+ 1
− 1
View file @ 58864e5b
...@@ -144,7 +144,7 @@ Section rwlockwriteguard_functions. ...@@ -144,7 +144,7 @@ Section rwlockwriteguard_functions.
iDestruct (GPS_SWWriter_shared with "W") as "[W Rs]". iDestruct (GPS_SWWriter_shared with "W") as "[W Rs]".
iSplitR ""; [|done]. iExists None. iSplitL ""; [done|]. iSplitR ""; [|done]. iExists None. iSplitL ""; [done|].
iFrame "Share g W Rs". iApply (bor_iff with "[] Hx'"). iFrame "Share g W Rs". iApply (bor_iff with "[] Hx'").
iIntros "!> !#". iApply bi_iff_sym. by iApply "EqO". } iIntros "!> !#". iApply bi.iff_sym. by iApply "EqO". }
{ by iIntros "!> !> $". } { by iIntros "!> !> $". }
iIntros "!>" (?) "(_ & R' & Hβ & _)". iIntros "!>" (?) "(_ & R' & Hβ & _)".
wp_seq. iMod ("Hcloseα" with "Hβ") as "Hα". wp_seq. iMod ("Hcloseα" with "Hβ") as "Hα".
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment