follow best practices for _CoqProject files

Core/Make

@@ -1,5 +1,9 @@
 -Q . DiSeL
--arg "-w -notation-overridden,-local-declaration,-redundant-canonical-projection,-projection-no-head-constant"
+
+-arg -w -arg -notation-overridden
+-arg -w -arg -local-declaration
+-arg -w -arg -redundant-canonical-projection
+-arg -w -arg -projection-no-head-constant
 
 Domain.v
 State.v

Core/opam

@@ -6,7 +6,7 @@ maintainer: "palmskog@gmail.com"
 homepage: "https://github.com/DistributedComponents/disel"
 dev-repo: "https://github.com/DistributedComponents/disel.git"
 bug-reports: "https://github.com/DistributedComponents/disel/issues"
-license: "BSD2"
+license: "BSD 2"
 
 build: [ make "-j" "%{jobs}%" ]
 install: [ make "install" ]
@@ -22,8 +22,9 @@ tags: [
   "keyword:program verification"
   "keyword:separation logic"
   "keyword:distributed algorithms"
+  "logpath:DiSeL"
 ]
 authors: [
-  "Ilya Sergey <>"
-  "James R. Wilcox <>"
+  "Ilya Sergey"
+  "James R. Wilcox"
 ]

Examples/Make

@@ -1,5 +1,9 @@
 -Q . DiSeL
--arg "-w -notation-overridden,-local-declaration,-redundant-canonical-projection,-projection-no-head-constant"
+
+-arg -w -arg -notation-overridden
+-arg -w -arg -local-declaration
+-arg -w -arg -redundant-canonical-projection
+-arg -w -arg -projection-no-head-constant
 
 Calculator/CalculatorInvariant.v
 Calculator/DelegatingCalculatorServer.v

LICENSE

@@ -1,4 +1,4 @@
-Copyright (c) 2016-2017, Distributed Components Team.
+Copyright (c) 2016-2018, Distributed Components Team.
 All rights reserved.
 
 Redistribution and use in source and binary forms, with or without
@@ -22,4 +22,4 @@ LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
-OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

README.md

@@ -11,8 +11,8 @@ Zachary Tatlock, in the POPL 2018 proceedings.
 
 ### Requirements
 
-* [Coq 8.7 or 8.8](https://coq.inria.fr)
-* [Mathematical Components 1.6.2 or later](http://math-comp.github.io/math-comp/) (`ssreflect`)
+* [Coq 8.7 or later](https://coq.inria.fr)
+* [Mathematical Components 1.6.2 or later](http://math-comp.github.io/math-comp/) (`ssreflect` suffices)
 * [FCSL PCM library 1.0.0 or later](https://github.com/imdea-software/fcsl-pcm)
 * [OCaml 4.05.0 or later](https://ocaml.org) (to compile and run the extracted applications)
 

_CoqProject

@@ -1,6 +1,10 @@
 -Q Core DiSeL
 -Q Examples DiSeL
--arg "-w -notation-overridden,-local-declaration,-redundant-canonical-projection,-projection-no-head-constant"
+
+-arg -w -arg -notation-overridden
+-arg -w -arg -local-declaration
+-arg -w -arg -redundant-canonical-projection
+-arg -w -arg -projection-no-head-constant
 
 Core/Domain.v
 Core/State.v