update documentation to mention the mczify dependency

README.md

@@ -12,7 +12,7 @@ Up-to-date documentation for all branches of the main Prosa repository is availa
 
 ## Publications
 
-Please see the [list of publications](http://prosa.mpi-sws.org/documentation.html#publications) on the Prosa project's homepage. 
+Please see the [list of publications](https://prosa.mpi-sws.org/publications.html) on the Prosa project's homepage. 
 
 ## Directory and Module Structure
 
@@ -37,7 +37,7 @@ All results published prior to 2020 build on this "classic" version of Prosa.
 
 ### With OPAM
 
-Prosa can be installed using the [OPAM package manager](https://opam.ocaml.org/) (>= 2.0)
+Prosa can be installed using the [OPAM package manager](https://opam.ocaml.org/) (>= 2.0).
 
 ```
 opam repo add coq-released https://coq.inria.fr/opam/released
@@ -46,6 +46,17 @@ opam update
 opam install coq-prosa
 ```
 
+### From Sources with `opam`
+
+OPAM can also be used to install a local checkout. For example, this is done in the CI setup (see `.gitlab-ci.yaml`).
+
+```
+opam repo add coq-released https://coq.inria.fr/opam/released
+opam update
+opam pin add -n -y -k path coq-prosa .
+opam install coq-prosa
+```
+
 ### From Sources With `esy`
 
 Prosa can be installed using [esy](https://esy.sh/).
@@ -74,13 +85,22 @@ Alternatively, `esy shell` opens a shell within its environment.
 
 #### Dependencies
 
-Besides Coq itself, Prosa's only external dependency is the ssreflect library of the [Mathematical Components project](https://math-comp.github.io).
+Besides on Coq itself, Prosa depends on 
+
+1. the `ssreflect` library of the [Mathematical Components project](https://math-comp.github.io) and
+2. the [Micromega support for the Mathematical Components library](https://github.com/math-comp/mczify) provided by `mczify`.
+
+These dependencies can be easily installed with OPAM.
+
+```
+opam install -y coq-mathcomp-ssreflect coq-mathcomp-zify
+```
 
 Prosa always tracks the latest stable versions of Coq and ssreflect. We do not maintain compatibility with older versions of either Coq or ssreflect.
 
 #### Compiling Prosa
 
-Assuming ssreflect is available (either via OPAM or compiled from source, see the [Prosa setup instructions](http://prosa.mpi-sws.org/setup-instructions.html)), compiling Prosa consists of only two steps.
+Assuming all dependencies are available (either via OPAM or compiled from source, see the [Prosa setup instructions](http://prosa.mpi-sws.org/setup-instructions.html)), compiling Prosa consists of only two steps.
 
 First, create an appropriate `Makefile`.
 

doc/tactics.md

@@ -24,11 +24,15 @@ Tactics taken from the standard library of Viktor Vafeiadis.
 
 - `have y := f x1 x2 x3`: creates an alias to `f x1 x2 x3` called `y` (in the local context). Note that `f` can be a function or a proposition/lemma. It's usually easier to read than `move: (f x1 x2 x3) => y`.
 
-*To be written… please feel free to start.*
+*To be continued… please help out.*
 
 ## Standard Coq Tactics
 
-*To be written… please feel free to start.*
+Generally speaking, in new code, prefer `ssreflect` tactics over standard Coq tactics whenever possible. While the current code base is a mix of classic Coq tactics and `ssreflect` tactics, that's only a historical accident not worth emulating. 
+
+- `lia`: Solves arithmetic goals, including ones with `ssreflect`'s definitions (thanks to the `coq-mathcomp-zify` dependency).
+
+*To be continued… please help out.*
 
 ## PROSA Tactics
 
@@ -37,7 +41,4 @@ Tactics taken from the standard library of Viktor Vafeiadis.
 - `interval_to_duration t1 t2 k`: any interval `[t1, t2]` can be represented as `[t1, t1 + k]` for some natural number `k`. This tactic searches for inequality `t1 <= t2` (or `t1 < t2`) in the context and replaces `t2` with `t1 + k`. Note: `k` is the name of a newly created natural number. 
 
 
-## Miscellaneous
-
-- `lia`: Solves arithmetic goals, including ones with `ssreflect`'s definitions.