Skip to content
Snippets Groups Projects
Commit 213fc044 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'fix-typo' into 'master'

CHANGELOG.md: Fix typo

See merge request !437
parents 7364ea6e 141bc42e
No related branches found
No related tags found
No related merge requests found
......@@ -131,7 +131,7 @@ Coq development, but not every API-breaking change is listed. Changes marked
`list_singletonM_length` -> `list_singleton_length`,
`list_alter_singletonM` -> `list_alter_singleton`,
`list_singletonM_included` -> `list_singleton_included`.
* New ASCII versions of Iris notations. These are marked printing only and
* New ASCII versions of Iris notations. These are marked parsing only and
can be made available using `Require Import iris.bi.ascii`. The new
notations are (notations marked [†] are disambiguated using notation scopes):
- entailment: `|--` for `⊢` and `-|-` for `⊣⊢`
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment