Commit 46643628 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Update README.

parent aa7e908d
......@@ -40,6 +40,9 @@ running:
language, e.g., parallel composition.
Most notable here s `lib/barrier`, the implementation and proof of a barrier
as described in <>.
* The folder `proofmode` contains the Iris proof mode, which extends Coq with
contexts for persistent and spatial Iris assertions. It also contains tactics
for interactive proofs in Iris.
* The folder `tests` contains modules we use to test our infrastructure.
Users of the Iris Coq library should *not* depend on these modules; they may
change or disappear without any notice.
Supports Markdown
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