From 141bc42e6e24740d3f630d1db05081b140c54317 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com> Date: Tue, 28 Apr 2020 14:42:06 +0200 Subject: [PATCH] CHANGELOG.md: Fix typo --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 3174c1738..701298e33 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 `⊣⊢` -- GitLab