Commit 76dd21ac authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'auth_rename' into 'master'

Add renaming for `auth`  to CHANGELOG

See merge request iris/iris!251
parents 8cea92ec 02b65ee9
...@@ -119,6 +119,19 @@ Changes in Coq: ...@@ -119,6 +119,19 @@ Changes in Coq:
authoritative elements have agreement: `✓ (●{p} a ⋅ ●{q} b) ⇒ a ≡ b`. As a authoritative elements have agreement: `✓ (●{p} a ⋅ ●{q} b) ⇒ a ≡ b`. As a
consequence, `auth` is no longer a COFE and does not preserve Leibniz consequence, `auth` is no longer a COFE and does not preserve Leibniz
equality. equality.
* Rename in `auth`:
- Use `auth_auth_proj`/`auth_frag_proj` for the projections of `auth`:
`authoritative``auth_auth_proj` and `auth_own``auth_frag_proj`.
- Use `auth_auth` and `auth_frag` for the injections into authoritative
elements and non-authoritative elements respectively.
- Lemmas for the projections and injections are renamed accordingly.
For examples:
+ `authoritative_validN``auth_auth_proj_validN`
+ `auth_own_validN``auth_frag_proj_validN`
+ `auth_auth_valid` was not renamed because it was already used for the
authoritative injection.
- `auth_both_valid``auth_both_valid_2`
- `auth_valid_discrete_2``auth_both_valid`
## Iris 3.1.0 (released 2017-12-19) ## 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