Commit 5425c9b1 authored by Ralf Jung's avatar Ralf Jung

some README changes

parent b6f2f9e2
Pipeline #5968 canceled with stages
......@@ -44,3 +44,11 @@ Changes to notations:
+ Change the level of the do-notation.
+ `<$>` is left associative.
+ Notation `x ;; y` for `_ ← x; y`.
## History
Coq-std++ has originally been developed by Robbert Krebbers as part of his
formalization of the C programming language in his PhD thesis, called
[CH2O](http://robbertkrebbers.nl/thesis.html). After that, Coq-std++ has been
part of the [Iris project](http://iris-project.org), and has continued to be
developed by Robbert Krebbers, Ralf Jung, and Jacques Henri-Jourdan.
......@@ -34,20 +34,22 @@ Notably:
`Obligation Tactic := idtac`, `Add Search Blacklist "_obligation_"`. See
[`base.v`](theories/base.v) for further details.
## History
Coq-std++ has originally been developed by Robbert Krebbers as part of his
formalization of the C programming language in his PhD thesis, called
[CH2O](http://robbertkrebbers.nl/thesis.html). After that, Coq-std++ has been
part of the [Iris project](http://iris-project.org), and has continued to be
developed by Robbert Krebbers, Ralf Jung, and Jacques Henri-Jourdan.
## Prerequisites
This version is known to compile with:
- Coq version 8.6.0 / 8.6.1 / 8.7.0 / 8.7.1
## Building Instructions
## Installing via opam
To obtain the latest stable release via opam, you have to add the Coq opam
repository:
opam repo add coq-released https://coq.inria.fr/opam/released
Then you can do `opam install coq-stdpp`.
## Building from source
Run `make` to build the full development. Run `make install` to install the library.
Run `make -jN` in this directory to build the library, where `N` is the number
of your CPU cores. Then run `make install` to install the library.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment