Update other connectives with dfrac.

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 *)

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.

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.

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 *)

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