From aadfe8343d404fee1abdab0bc47b13805de8d39b Mon Sep 17 00:00:00 2001
From: Simon Gregersen <gregersen@cs.au.dk>
Date: Fri, 10 Jul 2020 15:42:34 +0200
Subject: [PATCH] cleanup
---
.gitignore | 3 ++-
build-dep/opam | 16 ----------------
.../lib/serialization/serialization_base.v | 1 -
theories/aneris_lang/notation.v | 1 -
4 files changed, 2 insertions(+), 19 deletions(-)
delete mode 100644 build-dep/opam
diff --git a/.gitignore b/.gitignore
index a5dbdd0..f812305 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 d4a8059..0000000
--- 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 0957bef..ee9eb53 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 165018e..5925698 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
--
GitLab