Skip to content
Snippets Groups Projects
Commit 9b5ef3bf authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Bump

parent 148514c2
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
coq-lambda-rust.opam
+ 1
− 1
View file @ 9b5ef3bf
...@@ -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-06-27.0.bf367fe7") | (= "dev") } "coq-gpfsl" { (= "dev.2021-07-23.0.bc8c3ad9") | (= "dev") }
] ]
build: [make "-j%{jobs}%"] build: [make "-j%{jobs}%"]
......
theories/lifetime/model/creation.v
+ 0
− 1
View file @ 9b5ef3bf
...@@ -185,7 +185,6 @@ Proof. ...@@ -185,7 +185,6 @@ Proof.
assert (↑mgmtN ## userE) by solve_ndisj. set_solver. } assert (↑mgmtN ## userE) by solve_ndisj. set_solver. }
{ done. } { done. }
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose". iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
{ rewrite <-union_subseteq_l. solve_ndisj. }
iMod (ilft_create _ _ {[+ Λ +]} with "HA HI Hinv") as "H". clear A I. iMod (ilft_create _ _ {[+ Λ +]} with "HA HI Hinv") as "H". clear A I.
iDestruct "H" as (A I) "(% & HA & HI & Hinv)". iDestruct "H" as (A I) "(% & HA & HI & Hinv)".
rewrite /lft_tok /= big_sepMS_singleton. iDestruct "HΛ" as (V'0) "[#HV'0 HΛ]". rewrite /lft_tok /= big_sepMS_singleton. iDestruct "HΛ" as (V'0) "[#HV'0 HΛ]".
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment