Merge branch 'ralf/gmap_view' into 'master'

add gmap_view type notation (mirroring auth)

See merge request iris/iris!544

tests/algebra.v

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

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