updated readme again

Author: palmskog

README.md

@@ -1,5 +1,5 @@
 # InfSeqExt
-InfSeqExt is collection of Coq libraries for reasoning inductively and coinductively on infinite sequences, based on an [earlier library](http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=5198503) by Deng and Monin. InfSeqExt is intended as a more comprehensive alternative to [Streams](https://coq.inria.fr/library/Coq.Lists.Streams.html) in the Coq standard library. In particular, InfSeqExt provides machinery commonly used when reasoning about temporal properties of execution traces produced by distributed systems.
+`InfSeqExt` is collection of Coq libraries for reasoning inductively and coinductively on infinite sequences, based on an [earlier library](http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=5198503) by Deng and Monin. `InfSeqExt` is intended as a more comprehensive alternative to [`Streams`](https://coq.inria.fr/library/Coq.Lists.Streams.html) in the Coq standard library. In particular, `InfSeqExt` provides machinery commonly used when reasoning about temporal properties of system execution traces. The libraries have some overlap with the less exhaustive [`CTLTCTL`](https://github.com/coq-contribs/ctltctl) Coq contribution, which provides similar machinery. However, in contrast to `CTLTCTL`, `InfSeqExt` does not provide a definition of traces following some labeled reduction relation, nor an explicit notion of time.
 
 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 InfSeqExt will typically include `Require Import InfSeqExt.infseq.`