Update dependencies + some cleanup

coq-lambda-rust.opam

@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2021-10-01.1.8da490e3") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2021-10-03.0.63d7ad95") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]

theories/typing/lib/rwlock/rwlock.v

@@ -350,11 +350,7 @@ Section rwlock_inv.
   Lemma rwlock_interp_read_acq l t s v γ γs α tyO tyS tid:
     (▽{tid} rwlock_interp γs α tyO tyS false l γ t s v : vProp) -∗
       ∃ st, ⌜v = #(Z_of_rwlock_st st)⌝.
-  Proof.
-    iIntros "Int". iDestruct (acq_exist with "Int") as (?) "Int".
-    iDestruct (acq_sep_elim with "Int") as "[Int _]".
-    iDestruct (acq_pure_elim with "Int") as "?". iExists _. iFrame.
-  Qed.
+  Proof. iDestruct 1 as (?) "[% _]". by iExists _. Qed.
 
   Lemma rwlock_proto_change_tid_own l γ γs α tyS tyO tid_own1 tid_own2 tid_shr ty :
     Send ty →

theories/typing/lib/rwlock/rwlock_code.v

@@ -191,9 +191,7 @@ Section rwlock_functions.
       - iDestruct 1 as (st Eqvs) "F".
         iIntros "!>". iSplitR ""; iExists st; [by iFrame "F"|done].
       - iIntros (Eqvs) "!>". iSplit; [done|]. by iExists (Some (inl ())). }
-    iIntros "!>" (t' [] v') "(_ & #R' & Hβtok1 & Int)".
-    iDestruct (acq_exist with "Int") as (st') "Int".
-    iDestruct (acq_pure_elim with "Int") as %?. subst v'.
+    iIntros "!>" (t' [] v') "(_ & #R' & Hβtok1 & [%st' %])". subst v'.
     wp_let. wp_op; case_bool_decide as Hm1; wp_if.
     - iDestruct (monPred_objectively_elim with "Hβtok2") as "Hβtok2".
       iMod ("Hclose'" with "[$]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".

theories/typing/lib/rwlock/rwlockreadguard_code.v

@@ -89,9 +89,7 @@ Section rwlockreadguard_functions.
       - iDestruct 1 as (st Eqvs) "F".
         iIntros "!>". iSplitR ""; iExists st; [by iFrame "F"|done].
       - iIntros (Eqvs) "!>". iSplit; [done|]. by iExists (Some (inl ())). }
-    iIntros "!>" (t' [] v') "(_ & #R' & Hβ & Int)".
-    iDestruct (acq_exist with "Int") as (st2) "Int".
-    iDestruct (acq_pure_elim with "Int") as %?. subst v'. iClear "Int". clear tR vR.
+    iIntros "!>" (t' [] v') "(_ & #R' & Hβ & [%st2 %])". subst v'. clear tR vR.
 
     wp_let. wp_op. wp_bind (CAS _ _ _ _ _ _).
     set P : vProp Σ := (rwown γs (reading_st q ν) ∗ (q).[ν])%I.