diff --git a/tests/algebra.v b/tests/algebra.v
index cff006b35fb5dad5262206b75e9b9286d69c142f..d20708c8f85cd4663ffd664ea66e9e58e58a1b85 100644
--- a/tests/algebra.v
+++ b/tests/algebra.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Import auth excl.
+From iris.algebra Require Import auth excl lib.gmap_view.
 From iris.base_logic.lib Require Import invariants.
 
 (** Make sure that the same [Equivalence] instance is picked for Leibniz OFEs
@@ -48,3 +48,9 @@ Section test_prod.
     Persistent (PROP:=iPropI Σ) (own γ (◯((None, None), Some (to_agree true)))).
   Proof. apply _. Qed.
 End test_prod.
+
+(** Make sure the [auth]/[gmap_view] notation does not mix up its arguments. *)
+Definition auth_check {A : ucmraT} :
+  auth A = authO A := eq_refl.
+Definition gmap_view_check {K : Type} `{Countable K} {V : ofeT} :
+  gmap_view K V = gmap_viewO K V := eq_refl.
diff --git a/theories/algebra/lib/gmap_view.v b/theories/algebra/lib/gmap_view.v
index 49666bdcc3e03a57c3ebd6a18b8e02cf16684407..879c029e9c5dc54da4ff86b87a19b5c9bab1459a 100644
--- a/theories/algebra/lib/gmap_view.v
+++ b/theories/algebra/lib/gmap_view.v
@@ -122,12 +122,15 @@ End rel.
 
 Local Existing Instance gmap_view_rel_discrete.
 
-Definition gmap_viewUR (K : Type) `{Countable K} (V : ofeT) : ucmraT :=
-  viewUR (gmap_view_rel K V).
-Definition gmap_viewR (K : Type) `{Countable K} (V : ofeT) : cmraT :=
-  viewR (gmap_view_rel K V).
+(** [gmap_view] is a notation to give canonical structure search the chance
+to infer the right instances (see [auth]). *)
+Notation gmap_view K V := (view (@gmap_view_rel_raw K _ _ V)).
 Definition gmap_viewO (K : Type) `{Countable K} (V : ofeT) : ofeT :=
   viewO (gmap_view_rel K V).
+Definition gmap_viewR (K : Type) `{Countable K} (V : ofeT) : cmraT :=
+  viewR (gmap_view_rel K V).
+Definition gmap_viewUR (K : Type) `{Countable K} (V : ofeT) : ucmraT :=
+  viewUR (gmap_view_rel K V).
 
 Section definitions.
   Context {K : Type} `{Countable K} {V : ofeT}.