add gmap_view type notation (mirroring auth)

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}.