fix build

_CoqProject

@@ -63,9 +63,6 @@ theories/typing/lib/refcell/ref_code.v
 theories/typing/lib/refcell/refmut_code.v
 theories/typing/lib/refcell/refmut.v
 theories/typing/lib/refcell/ref.v
-theories/typing/lib/rwlock/rwlock.v
-theories/typing/lib/rwlock/rwlockreadguard.v
-theories/typing/lib/rwlock/rwlockwriteguard.v
 theories/typing/examples/get_x.v
 theories/typing/examples/rebor.v
 theories/typing/examples/unbox.v

theories/lang/lock.v

@@ -7,7 +7,9 @@ Set Default Proof Using "Type".
 
 Definition mklock_unlocked : val := λ: ["l"], "l" <- #false.
 Definition mklock_locked : val := λ: ["l"], "l" <- #true.
-Definition try_acquire : val := λ: ["l"], CAS "l" #false #true AcqRel Relaxed.
+(* If the CAS fails, it's a relaxed-read.
+   If the CAS succeeds, it's a acq-read and relaxed-write *)
+Definition try_acquire : val := λ: ["l"], CAS "l" #false #true Relaxed AcqRel Relaxed.
 Definition acquire : val :=
   rec: "acquire" ["l"] := if: try_acquire ["l"] then #☠ else "acquire" ["l"].
 Definition release : val := λ: ["l"], "l" <-ʳᵉˡ #false.
@@ -135,9 +137,9 @@ Section proof.
     wp_rec. iMod ("Hproto" with "HP") as (γ R0 Vb) "(#[Eq lc] & inv & Hclose)".
     iDestruct "lc" as (?) "lc".
     iMod (rel_True_intro True%I tid with "[//]") as "rTrue".
-    iApply (GPS_PPRaw_CAS_simple (lock_interp R0) _ _ _ _
+    iApply (GPS_PPRaw_CAS_int_simple (lock_interp R0) _ _ _ _ _
                 (Z_of_bool false) #true () (λ _, R0)%I (λ _ _, True)%I
-            with "[$lc $inv rTrue]"); [done|by right|by left|..].
+            with "[$lc $inv rTrue]");[done|by left|done|by right|by left|..].
     { iSplitL ""; [|iSplitL ""]; [iNext; iModIntro..|].
       - iIntros (?? _). by iApply lock_interp_comparable.
       - by iIntros (??)"_ #$".