diff --git a/.gitignore b/.gitignore
index a5dbdd07acc077aee5dc3104f119bd59ccb799f2..f8123050d9eeeec5fe31f0859720ac1729fc59a9 100644
--- a/.gitignore
+++ b/.gitignore
@@ -35,6 +35,7 @@ nra.cache
 Makefile.coq.conf
 CoqMakefile.conf
 Makefile.coq
+build-dep/
 
 ### Emacs ###
 # -*- mode: gitignore; -*-
@@ -113,4 +114,4 @@ Icon
 .AppleDesktop
 Network Trash Folder
 Temporary Items
-.apdisk
\ No newline at end of file
+.apdisk
diff --git a/build-dep/opam b/build-dep/opam
deleted file mode 100644
index d4a8059fc66c8e96d9b0ccfe5ecc9821a56050e6..0000000000000000000000000000000000000000
--- a/build-dep/opam
+++ /dev/null
@@ -1,16 +0,0 @@
-opam-version: "2.0"
-name: "coq-aneris-builddep"
-synopsis: "This is the Coq development of the Aneris program logic"
-maintainer: "Simon Gregersen <gregersen@cs.au.dk>"
-authors: "The Aneris Team"
-homepage: "https://iris-project.org/"
-dev-repo: "git+https://bitbucket.org/logsem/aneris.git"
-bug-reports: "https://bitbucket.org/logsem/aneris/issues"
-build: []
-install: []
-depends: [
-  "coq" { (= "8.11.2") | (= "dev") }
-  "coq-iris" { (= "dev.2020-07-04.0.e2639ac1") | (= "dev") }
-  "coq-stdpp" { (= "dev.2020-07-02.1.c8129a37") | (= "dev") }
-  "coq-iris-string-ident" { (= "dev") | (= "dev") }
-]
diff --git a/theories/aneris_lang/lib/serialization/serialization_base.v b/theories/aneris_lang/lib/serialization/serialization_base.v
index 0957bef9395ccf685d41bf0de018c6e5216f1a50..ee9eb53231a0d0eb0950182222146445a4c83955 100644
--- a/theories/aneris_lang/lib/serialization/serialization_base.v
+++ b/theories/aneris_lang/lib/serialization/serialization_base.v
@@ -147,7 +147,6 @@ Section strings.
 
 End strings.
 
-(* @Amin TODO : (de)serialisation of write events *)
 Section library.
   Context `{dG : distG Σ}.
 
diff --git a/theories/aneris_lang/notation.v b/theories/aneris_lang/notation.v
index 165018e1234ad8f1142c4c18d8d0deb4b644ccff..59256986294853ca769560b5e9cb51c94df4be98 100644
--- a/theories/aneris_lang/notation.v
+++ b/theories/aneris_lang/notation.v
@@ -39,7 +39,6 @@ Coercion ground_lang.of_val : ground_lang.val >-> ground_lang.expr.
 
 Coercion Var : string >-> ground_lang.expr.
 
-(* TODO: come up with something better... *)
 (* Note that the scope for expressions and values are NOT the same:
    Expressions have brackets that comes from the sequence \<, with name
    MATHEMATICAL LEFT ANGLE BRACKET where as values has brackets