Commit 02b65ee9 authored by Hai Dang's avatar Hai Dang
Browse files

More rename

parent a9ead9a3
......@@ -125,6 +125,11 @@ Changes in Coq:
- 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`
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