updated README.md and Travis downstream

Author: palmskog

.travis-ci.sh

@@ -6,7 +6,7 @@ opam install coq.$COQ_VERSION --yes --verbose
 ./build.sh
 
 case $DOWNSTREAM in
-verdi)
+verdi-aggregation)
   opam install coq-mathcomp-ssreflect.$SSREFLECT_VERSION --yes --verbose
 
   pushd ..
@@ -19,6 +19,16 @@ verdi)
     pushd verdi
       ./build.sh
     popd
+
+    git clone -b v8.5 'https://github.com/coq-contribs/aac-tactics.git' AAC_tactics
+    pushd AAC_tactics
+      make
+    popd
+
+    git clone 'https://github.com/DistributedComponents/verdi-aggregation.git'
+    pushd verdi-aggregation
+      ./build.sh
+    popd
   popd
   ;;
 esac

.travis.yml

@@ -14,7 +14,7 @@ env:
     - SSREFLECT_VERSION=1.6
   matrix:
     - DOWNSTREAM=none
-    - DOWNSTREAM=verdi
+    - DOWNSTREAM=verdi-aggregation
 sudo: false
 notifications:
   email: false

README.md

@@ -12,36 +12,29 @@ The libraries have some overlap with the less exhaustive [`CTLTCTL`](https://git
 Requirements
 ------------
 
-[`Coq 8.5`](https://coq.inria.fr/download)
+- [`Coq 8.5`](https://coq.inria.fr/download)
 
 Building
 --------
 
 This project uses [`coqproject.sh`](https://github.com/dwoos/coqproject) for dependency management. To build the libraries, first run `./configure` in the base directory and then run `make`. When added as a dependency to another project using `coqproject.sh`, the namespace is `InfSeqExt`, so Coq files that rely on the libraries will typically include `Require Import InfSeqExt.infseq.`
 
-infseq
-------
-This file contains the main definitions and results:
-* coinductive definition of infinite sequences
-* definitions and notations for modal operators and connectors
-  - basic modal operators: `now`, `next`, `consecutive`, `always1`, `always`, `weak_until`, `until`, `release`, `eventually`
-  - composite modal operators: `inf_often`, `continuously`
-  - modal connectors: `impl_tl` (`->_`), `and_tl` (`/\_`), `or_tl` (`\/_`), `not_tl` (`~_`)
-* lemmas about modal operators and connectors
-* tactics
-
-map
----
-This file contains corecursive definitions of the `map` and `zip` functions for use on infinite sequences, and related lemmas.
-
-exteq
+Files
 -----
-This file contains a coinductive definition of extensional equality (`exteq`) for infinite sequences, and related lemmas.
 
-subseq
-------
-This file contains coinductive definitions of infinite subsequences and related lemmas.
+- `infseq.v`: contains the main definitions and results.
+    * coinductive definition of infinite sequences
+    * definitions and notations for modal operators and connectors
+        - basic modal operators: `now`, `next`, `consecutive`, `always1`, `always`, `weak_until`, `until`, `release`, `eventually`
+        - composite modal operators: `inf_often`, `continuously`
+        - modal connectors: `impl_tl` (`->_`), `and_tl` (`/\_`), `or_tl` (`\/_`), `not_tl` (`~_`)
+    * lemmas about modal operators and connectors
+    * tactics
 
-classical
----------
-This file contains lemmas about modal operators and connectors when assuming classical logic (excluded middle).
+- `map.v`: contains corecursive definitions of the `map` and `zip` functions for use on infinite sequences, and related lemmas.
+
+- `exteq.v`: contains a coinductive definition of extensional equality (`exteq`) for infinite sequences, and related lemmas.
+
+- `subseq.v`: contains coinductive definitions of infinite subsequences and related lemmas.
+
+- `classical.v`: contains lemmas about modal operators and connectors when assuming classical logic (excluded middle).