From f0ce565d0f90c14544e101807b6b5ddf2693ce6d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 13 Feb 2023 10:27:16 +0100
Subject: [PATCH] Update other connectives with dfrac.

---
 iris/algebra/auth.v             |  8 ++------
 iris/algebra/lib/mono_list.v    | 10 ++--------
 iris/algebra/lib/mono_nat.v     | 10 ++--------
 iris/algebra/view.v             |  8 ++------
 iris/base_logic/lib/ghost_map.v | 13 +++----------
 5 files changed, 11 insertions(+), 38 deletions(-)

diff --git a/iris/algebra/auth.v b/iris/algebra/auth.v
index ea3f9e371..369315fca 100644
--- a/iris/algebra/auth.v
+++ b/iris/algebra/auth.v
@@ -70,12 +70,8 @@ Typeclasses Opaque auth_auth auth_frag.
 Global Instance: Params (@auth_auth) 2 := {}.
 Global Instance: Params (@auth_frag) 1 := {}.
 
-(** FIXME: Refactor these notations using custom entries once Coq bug #13654
-has been fixed. *)
-Notation "●{ dq } a" := (auth_auth dq a) (at level 20, format "●{ dq }  a").
-Notation "●{# q } a" := (auth_auth (DfracOwn q) a) (at level 20, format "●{# q }  a").
-Notation "●□ a" := (auth_auth (DfracDiscarded) a) (at level 20).
-Notation "● a" := (auth_auth (DfracOwn 1) a) (at level 20).
+Notation "● dq a" := (auth_auth dq a)
+  (at level 20, dq custom dfrac at level 1, format "● dq  a").
 Notation "â—¯ a" := (auth_frag a) (at level 20).
 
 (** * Laws of the authoritative camera *)
diff --git a/iris/algebra/lib/mono_list.v b/iris/algebra/lib/mono_list.v
index 9f453595c..16604065a 100644
--- a/iris/algebra/lib/mono_list.v
+++ b/iris/algebra/lib/mono_list.v
@@ -16,14 +16,8 @@ Global Instance: Params (@mono_list_auth) 2 := {}.
 Global Instance: Params (@mono_list_lb) 1 := {}.
 Typeclasses Opaque mono_list_auth mono_list_lb.
 
-(** FIXME: Refactor these notations using custom entries once Coq bug #13654
-has been fixed. *)
-Notation "●ML{ dq } l" :=
-  (mono_list_auth dq l) (at level 20, format "●ML{ dq }  l").
-Notation "●ML{# q } l" :=
-  (mono_list_auth (DfracOwn q) l) (at level 20, format "●ML{# q }  l").
-Notation "●ML□ l" := (mono_list_auth DfracDiscarded l) (at level 20).
-Notation "●ML l" := (mono_list_auth (DfracOwn 1) l) (at level 20).
+Notation "●ML dq l" := (mono_list_auth dq l)
+  (at level 20, dq custom dfrac at level 1, format "●ML dq  l").
 Notation "â—¯ML l" := (mono_list_lb l) (at level 20).
 
 Section mono_list_props.
diff --git a/iris/algebra/lib/mono_nat.v b/iris/algebra/lib/mono_nat.v
index 100b000b7..9c357aac0 100644
--- a/iris/algebra/lib/mono_nat.v
+++ b/iris/algebra/lib/mono_nat.v
@@ -17,14 +17,8 @@ Definition mono_nat_auth (dq : dfrac) (n : nat) : mono_nat :=
   ●{dq} MaxNat n ⋅ ◯ MaxNat n.
 Definition mono_nat_lb (n : nat) : mono_nat := â—¯ MaxNat n.
 
-(** FIXME: Refactor these notations using custom entries once Coq bug #13654
-has been fixed. *)
-Notation "●MN{ dq } a" :=
-  (mono_nat_auth dq a) (at level 20, format "●MN{ dq }  a").
-Notation "●MN{# q } a" :=
-  (mono_nat_auth (DfracOwn q) a) (at level 20, format "●MN{# q }  a").
-Notation "●MN□ a" := (mono_nat_auth DfracDiscarded a) (at level 20, format "●MN□  a").
-Notation "●MN a" := (mono_nat_auth (DfracOwn 1) a) (at level 20).
+Notation "●MN dq a" := (mono_nat_auth dq a)
+  (at level 20, dq custom dfrac at level 1, format "●MN dq  a").
 Notation "â—¯MN a" := (mono_nat_lb a) (at level 20).
 
 Section mono_nat.
diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index 85ec57056..baf5a6233 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -92,12 +92,8 @@ Typeclasses Opaque view_auth view_frag.
 Global Instance: Params (@view_auth) 3 := {}.
 Global Instance: Params (@view_frag) 3 := {}.
 
-(** FIXME: Refactor these notations using custom entries once Coq bug #13654
-has been fixed. *)
-Notation "●V{ dq } a" := (view_auth dq a) (at level 20, format "●V{ dq }  a").
-Notation "●V{# q } a" := (view_auth (DfracOwn q) a) (at level 20, format "●V{# q }  a").
-Notation "●V□ a" := (view_auth DfracDiscarded a) (at level 20, format "●V□  a").
-Notation "●V a" := (view_auth (DfracOwn 1) a) (at level 20).
+Notation "●V dq a" := (view_auth dq a)
+  (at level 20, dq custom dfrac at level 1, format "●V dq  a").
 Notation "â—¯V a" := (view_frag a) (at level 20).
 
 (** * The OFE structure *)
diff --git a/iris/base_logic/lib/ghost_map.v b/iris/base_logic/lib/ghost_map.v
index 5611fb729..2a9aa9744 100644
--- a/iris/base_logic/lib/ghost_map.v
+++ b/iris/base_logic/lib/ghost_map.v
@@ -45,16 +45,9 @@ Section definitions.
     @ghost_map_elem = @ghost_map_elem_def := ghost_map_elem_aux.(seal_eq).
 End definitions.
 
-(** FIXME: Refactor these notations using custom entries once Coq bug #13654
-has been fixed. *)
-Notation "k ↪[ γ ]{ dq } v" := (ghost_map_elem γ k dq v)
-  (at level 20, γ at level 50, dq at level 50, format "k  ↪[ γ ]{ dq }  v") : bi_scope.
-Notation "k ↪[ γ ]{# q } v" := (k ↪[γ]{DfracOwn q} v)%I
-  (at level 20, γ at level 50, q at level 50, format "k  ↪[ γ ]{# q }  v") : bi_scope.
-Notation "k ↪[ γ ] v" := (k ↪[γ]{#1} v)%I
-  (at level 20, γ at level 50, format "k  ↪[ γ ]  v") : bi_scope.
-Notation "k ↪[ γ ]□ v" := (k ↪[γ]{DfracDiscarded} v)%I
-  (at level 20, γ at level 50) : bi_scope.
+Notation "k ↪[ γ ] dq v" := (ghost_map_elem γ k dq v)
+  (at level 20, γ at level 50, dq custom dfrac at level 1,
+   format "k  ↪[ γ ] dq  v") : bi_scope.
 
 Local Ltac unseal := rewrite
   ?ghost_map_auth_unseal /ghost_map_auth_def
-- 
GitLab