Commit 8c7c1ba2 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files


parent f2be3543
......@@ -38,6 +38,8 @@ With this release, we dropped support for Coq 8.9.
`auth_auth_valid*`, `auth_frag_valid*`, or `auth_both_valid*` instead.
* Add the camera of discardable fractions `dfrac`. This is a generalization of
the normal fractional camera. See `theories/algebra/dfrac.v` for further information.
* Rename `cmra_monotone_valid` into `cmra_morphism_valid` (this rename was
forgotten in !56).
**Changes in `proofmode`:**
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