diff --git a/CHANGELOG.md b/CHANGELOG.md index 26f8e7cb1c288d876dc378e47693106668377365..7ec06e5f684e85d0195f78fff274351e9358288d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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. diff --git a/README.md b/README.md index 184d8eb1966d9b1b552b3d9c69241b6eda263a9f..f9f167504c1805471bfeca4279f040f755b19fdc 100644 --- a/README.md +++ b/README.md @@ -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.