Add some FIXMES.

iris/base_logic/lib/gen_heap.v

@@ -123,6 +123,8 @@ Section definitions.
 End definitions.
 Arguments meta {L _ _ V Σ _ A _ _} l N x.
 
+(** FIXME: Refactor these notations using custom entries once Coq bug #13654
+has been fixed. *)
 Local Notation "l ↦{ dq } v" := (mapsto l dq v)
   (at level 20, format "l  ↦{ dq }  v") : bi_scope.
 Local Notation "l ↦□ v" := (mapsto l DfracDiscarded v)

iris_heap_lang/derived_laws.v

@@ -16,6 +16,9 @@ with lists of values. *)
 
 Definition array `{!heapG Σ} (l : loc) (dq : dfrac) (vs : list val) : iProp Σ :=
   ([∗ list] i ↦ v ∈ vs, (l +ₗ i) ↦{dq} v)%I.
+
+(** FIXME: Refactor these notations using custom entries once Coq bug #13654
+has been fixed. *)
 Notation "l ↦∗{ dq } vs" := (array l dq vs)
   (at level 20, format "l  ↦∗{ dq }  vs") : bi_scope.
 Notation "l ↦∗□ vs" := (array l DfracDiscarded vs)

iris_heap_lang/lib/atomic_heap.v

@@ -48,21 +48,23 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
 Arguments atomic_heap _ {_}.
 
 (** Notation for heap primitives, in a module so you can import it separately. *)
+(** FIXME: Refactor these notations using custom entries once Coq bug #13654
+has been fixed. *)
 Module notation.
-Notation "l ↦{ dq } v" := (mapsto l dq v)
-  (at level 20, format "l  ↦{ dq }  v") : bi_scope.
-Notation "l ↦□ v" := (mapsto l DfracDiscarded v)
-  (at level 20, format "l  ↦□  v") : bi_scope.
-Notation "l ↦{# q } v" := (mapsto l (DfracOwn q) v)
-  (at level 20, format "l  ↦{# q }  v") : bi_scope.
-Notation "l ↦ v" := (mapsto l (DfracOwn 1) v)
-  (at level 20, format "l  ↦  v") : bi_scope.
-
-Notation "'ref' e" := (alloc e) : expr_scope.
-Notation "! e" := (load e) : expr_scope.
-Notation "e1 <- e2" := (store e1 e2) : expr_scope.
-
-Notation CAS e1 e2 e3 := (Snd (cmpxchg e1 e2 e3)).
+  Notation "l ↦{ dq } v" := (mapsto l dq v)
+    (at level 20, format "l  ↦{ dq }  v") : bi_scope.
+  Notation "l ↦□ v" := (mapsto l DfracDiscarded v)
+    (at level 20, format "l  ↦□  v") : bi_scope.
+  Notation "l ↦{# q } v" := (mapsto l (DfracOwn q) v)
+    (at level 20, format "l  ↦{# q }  v") : bi_scope.
+  Notation "l ↦ v" := (mapsto l (DfracOwn 1) v)
+    (at level 20, format "l  ↦  v") : bi_scope.
+
+  Notation "'ref' e" := (alloc e) : expr_scope.
+  Notation "! e" := (load e) : expr_scope.
+  Notation "e1 <- e2" := (store e1 e2) : expr_scope.
+
+  Notation CAS e1 e2 e3 := (Snd (cmpxchg e1 e2 e3)).
 
 End notation.
 

iris_heap_lang/primitive_laws.v

@@ -28,6 +28,8 @@ Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := {
 
 (** Since we use an [option val] instance of [gen_heap], we need to overwrite
 the notations.  That also helps for scopes and coercions. *)
+(** FIXME: Refactor these notations using custom entries once Coq bug #13654
+has been fixed. *)
 Notation "l ↦{ dq } v" := (mapsto (L:=loc) (V:=option val) l dq (Some v%V))
   (at level 20, format "l  ↦{ dq }  v") : bi_scope.
 Notation "l ↦□ v" := (mapsto (L:=loc) (V:=option val) l DfracDiscarded (Some v%V))