Commit 31288fa3 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files


parent 151dda05
......@@ -140,6 +140,9 @@ Changes in Coq:
authoritative injection.
- `auth_both_valid``auth_both_valid_2`
- `auth_valid_discrete_2``auth_both_valid`
* Add the camera `ufrac` for unbounded fractions (i.e. without fractions that
can be `> 1`) and the camera `ufrac_auth` for a variant of the authoritative
fractional camera (`frac_auth`) with unbounded fractions.
## Iris 3.1.0 (released 2017-12-19)
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