From 803e091ea314b51caaebe11c39712a93194da374 Mon Sep 17 00:00:00 2001
From: Gregory Malecha <gmalecha@gmail.com>
Date: Thu, 2 Apr 2020 15:10:43 +0200
Subject: [PATCH] adding fixme

---
 CHANGELOG.md        | 10 +++++-----
 theories/bi/ascii.v | 10 ++++++----
 2 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index ca0de4e5e..082fded0d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -150,10 +150,10 @@ s/\blist_singletonM_included\b/list_singleton_included/g
 
 * New ASCII versions of Iris notations. These are marked printing only and
   can be made available using `Require Import iris.bi.ascii`. The new
-  notation is († disambiguated using notation scopes):
+  notations are (notations marked [†] are disambiguated using notation scopes):
   - entailment: `|--` for `⊢` and `-|-` for `⊣⊢`
-  - logic†: `->` for `→`, `/\\` for `∧`, `\\/` for `∨`, and `<->` for `↔`
-  - quantifiers†: `forall` for `∀` and `exists` for `∃`
+  - logic[†]: `->` for `→`, `/\\` for `∧`, `\\/` for `∨`, and `<->` for `↔`
+  - quantifiers[†]: `forall` for `∀` and `exists` for `∃`
   - separation logic: `**` for `∗`, `-*` for `-∗`, and `*-*` for `∗-∗`
   - step indexing: `|>` for `â–·`
   - modalities: `<intuit>` for `â–¡` and `<except_0>` for `â—‡`
@@ -165,8 +165,8 @@ s/\blist_singletonM_included\b/list_singleton_included/g
     - `P ={E1,E2}=* Q` for `P ={E1,E2}=∗ Q`
     - `|={E1,E2,E3}|>=> Q` for `|={E1,E2,E3}â–·=> Q`
     - `|={E1,E2}|>=>^n Q` for `|={E1,E2}â–·=>^n Q`
-    The full list can be found in [theories/bi/ascii.v](theories/bi/ascii.v), where the ASCII notations
-    are defined in terms of the unicode notations.
+    The full list can be found in [theories/bi/ascii.v](theories/bi/ascii.v),
+    where the ASCII notations are defined in terms of the unicode notations.
 
 **Changes in heap_lang:**
 
diff --git a/theories/bi/ascii.v b/theories/bi/ascii.v
index 4c18c3fa6..725f06a14 100644
--- a/theories/bi/ascii.v
+++ b/theories/bi/ascii.v
@@ -2,22 +2,24 @@ From iris.bi Require Import interface derived_connectives updates.
 From iris.algebra Require Export ofe.
 
 (** note: we use [|--] instead of [|-] because the latter is used by
-    Ltac's [match goal] construct
+    Ltac's [match goal] construct.
  *)
 Notation "P |-- Q" := (P ⊢ Q)
   (at level 99, Q at level 200, right associativity, only parsing) : stdpp_scope.
 Notation "P '|--@{' PROP } Q" := (P ⊢@{PROP} Q) (at level 99, Q at level 200, right associativity, only parsing) : stdpp_scope.
 Notation "(|--)" := (⊢) (only parsing) : stdpp_scope.
+(* FIXME: fix notation *)
 Notation "('|--@{' PROP } )" := (bi_entails (PROP:=PROP)) (only parsing) : stdpp_scope.
 
+Notation "|-- Q" := (⊢ Q%I) (at level 20, Q at level 200, only parsing) : stdpp_scope.
+Notation "'|--@{' PROP } Q" := (⊢@{PROP} Q) (at level 20, Q at level 200, only parsing) : stdpp_scope.
+
 Notation "P -|- Q" := (P ⊣⊢ Q) (at level 95, no associativity, only parsing) : stdpp_scope.
 Notation "P '-|-@{' PROP } Q" := (P ⊣⊢@{PROP} Q) (at level 95, no associativity, only parsing) : stdpp_scope.
 Notation "(-|-)" := (⊣⊢) (only parsing) : stdpp_scope.
+(* FIXME: fix notation *)
 Notation "('-|-@{' PROP } )" := (equiv (A:=bi_car PROP)) (only parsing) : stdpp_scope.
 
-Notation "|-- Q" := (⊢ Q%I) (at level 20, Q at level 200, only parsing) : stdpp_scope.
-Notation "'|--@{' PROP } Q" := (⊢@{PROP} Q) (at level 20, Q at level 200, only parsing) : stdpp_scope.
-
 Notation "P -* Q" := (P ⊢ Q)%stdpp (at level 99, Q at level 200, right associativity, only parsing) : stdpp_scope.
 
 (* FIXME: Notation "'⌜' φ '⌝'" := (bi_pure φ%type%stdpp) : bi_scope. *)
-- 
GitLab