diff --git a/theories/algebra/lib/gmap_view.v b/theories/algebra/lib/gmap_view.v
index abe12c6cf741da058db9b4268c2c98530b101457..d94c5caa4a62c0ab44c092528a1604c67b898912 100644
--- a/theories/algebra/lib/gmap_view.v
+++ b/theories/algebra/lib/gmap_view.v
@@ -94,12 +94,19 @@ 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).
+
+(** Make sure the notation does not mix up its arguments. *)
+Local Definition gmap_view_check {K : Type} `{Countable K} {V : ofeT} :
+  gmap_view K V = gmap_viewO K V := eq_refl.
 
 Section definitions.
   Context {K : Type} `{Countable K} {V : ofeT}.