diff --git a/README.md b/README.md
index 82ed7882dd268bac67af365fb79581748dbd1b61..4c10b5ae8f960748a46613edd714f9104804f322 100644
--- a/README.md
+++ b/README.md
@@ -6,8 +6,4 @@ Atomicity related verification based on Iris logic.
 Build
 --------
 
-1. `git clone` this repo
-2. `git submodule update --init` to fetch corresponding Iris library as a submodule
-3. `cd iris-coq; make; make install` to install Iris library (system globally). Or you can use `make userinstall` to install user globally.
-4. `cd ..; make` to compile this repo
-
+Please make sure Iris dependency version is same as noted in `IRIS_VERSION`
diff --git a/atomic_sync.v b/atomic_sync.v
index d5e33f055b6c735c25824e4030d9d81c33a222f7..8eb17c47a06f2ae9e68668fb7b2649d0b313b720 100644
--- a/atomic_sync.v
+++ b/atomic_sync.v
@@ -28,7 +28,7 @@ Section atomic_sync.
                                 (f x) (P x) (fun _ => Q x))%I.
        
   Definition sync (mk_syncer: val) : val :=
-    λ: "f_cons" "f_seq" "l",
+    λ: "f_seq" "l",
        let: "s" := mk_syncer #() in
        "s" ("f_seq" "l").
 
@@ -51,12 +51,12 @@ Section atomic_sync.
       heapN ⊥ N →
       heap_ctx ★ R ★ (∀ s, □ (is_syncer R s) -★ Φ s) ⊢ WP mk_syncer #() {{ Φ }}.
   
-  Lemma atomic_spec (mk_syncer f_cons f_seq l: val) (ϕ: val → A → iProp Σ) α β Ei:
+  Lemma atomic_spec (mk_syncer f_seq l: val) (ϕ: val → A → iProp Σ) α β Ei:
       ∀ (g0: A),
         heapN ⊥ N → seq_spec f_seq ϕ α β ⊤ →
         mk_syncer_spec mk_syncer →
         heap_ctx ★ ϕ l g0
-        ⊢ WP (sync mk_syncer) f_cons f_seq l {{ f, ∃ γ, gHalf γ g0 ★ ∀ x, □ atomic_triple' α β Ei ⊤ f x γ  }}.
+        ⊢ WP (sync mk_syncer) f_seq l {{ f, ∃ γ, gHalf γ g0 ★ ∀ x, □ atomic_triple' α β Ei ⊤ f x γ  }}.
   Proof.
     iIntros (g0 HN Hseq Hsync) "[#Hh HÏ•]".
     iVs (own_alloc (((1 / 2)%Qp, DecAgree g0) ⋅ ((1 / 2)%Qp, DecAgree g0))) as (γ) "[Hg1 Hg2]".