update dependencies

opam

@@ -16,7 +16,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2020-03-21.0.2d3787d5") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2020-04-04.0.848c1c07") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]

theories/lifetime/model/accessors.v

@@ -78,7 +78,7 @@ Proof.
     [by rewrite Hf2 Hf1|by apply Hhv2, Hhv1].
   - clear. iIntros (Λ HΛ A) "Htok HA". iDestruct "Htok" as (V') "[% Htok]".
     iDestruct (own_valid_2 with "HA Htok") as
-        %[(s0 & Hv & Hincl)%singleton_included _]%auth_both_valid.
+        %[(s0 & Hv & Hincl)%singleton_included_l _]%auth_both_valid.
     revert Hv Hincl. rewrite lookup_fmap. case HA: (A!!Λ)=>[[b V'']|]; [|by inversion 1].
     move=> <- /Some_included Hincl. destruct b; last first.
     { case Hincl=>[|/csum_included]; [by inversion 1|]. naive_solver. }
@@ -101,7 +101,7 @@ Proof.
     iAssert (⌜lft_has_view A' κ V⌝)%I as %HA'V.
     { iIntros (Λ HΛ). iDestruct (@big_sepMS_elem_of with "Htok") as "Htok"=>//.
       iDestruct (own_valid_2 with "HA' Htok")
-        as %[(s & HA' & [Hs|Hs]%Some_included)%singleton_included _]%auth_both_valid.
+        as %[(s & HA' & [Hs|Hs]%Some_included)%singleton_included_l _]%auth_both_valid.
       - setoid_subst. rewrite lookup_fmap /to_lft_stateR in HA'.
         destruct (A'!!Λ) as [[[] V']|]=>/=.
         + apply (inj Some), (inj Cinl), (inj2 pair), proj2, (inj to_latT) in HA'=>//.
@@ -171,7 +171,7 @@ Proof.
   iDestruct "Hinv" as (Vκ) "[>% [[Hinv >%]|[Hinv >%]]]"; last first.
   { iDestruct "Hinv" as (??) "(_ & Hinv & _)". iDestruct "Hinv" as (B ?) "[>Hinv _]".
     iDestruct (own_bor_valid_2 with "Hinv Hf")
-      as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_both_valid.
+      as %[(_ & <- & INCL%option_included)%singleton_included_l _]%auth_both_valid.
     exfalso. destruct INCL as [[=]|(? & ? & [=<-] & Hi & Ho)].
     rewrite lookup_fmap in Hi. destruct (B !! s); inversion Hi; subst; clear Hi.
     by destruct Ho as [?%(inj Excl)|?%(exclusive_included _)]. }
@@ -273,7 +273,7 @@ Proof.
   iDestruct "Hinv" as (Vκ) "[>% [[Hinv >%]|[Hinv >%]]]"; last first.
   { iDestruct "Hinv" as (??) "(_ & Hinv & _)". iDestruct "Hinv" as (B ?) "[>Hinv _]".
     iDestruct (own_bor_valid_2 with "Hinv Hbor")
-      as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_both_valid.
+      as %[(_ & <- & INCL%option_included)%singleton_included_l _]%auth_both_valid.
     exfalso. destruct INCL as [[=]|(? & ? & [=<-] & Hi & Ho)].
     rewrite lookup_fmap /= in Hi. destruct (B !! s''); inversion Hi; subst; clear Hi.
     by destruct Ho as [?%(inj Excl)|?%(exclusive_included _)]. }

theories/lifetime/model/creation.v

@@ -184,7 +184,7 @@ Proof.
   iDestruct "H" as (A I) "(% & HA & HI & Hinv)".
   rewrite /lft_tok /= big_sepMS_singleton. iDestruct "HΛ" as (V'0) "[#HV'0 HΛ]".
   iDestruct (own_valid_2 with "HA HΛ")
-    as %[[s [Hs Hincl%Some_included]]%singleton_included Hv]%auth_both_valid.
+    as %[[s [Hs Hincl%Some_included]]%singleton_included_l Hv]%auth_both_valid.
   destruct Hincl; last first.
   { destruct (exclusive_included (Cinl (1%Qp, to_latT V'0)) s)=>//.
     move: (Hv Λ). by rewrite Hs. }

theories/lifetime/model/primitive.v

@@ -25,7 +25,7 @@ Implicit Types κ : lft.
 Lemma to_borUR_included (B : gmap slice_name (bor_state Lat)) i s :
   {[i := Excl s]} ≼ to_borUR B → B !! i = Some s.
 Proof.
-  rewrite singleton_included=> -[qs []]. unfold_leibniz.
+  rewrite singleton_included_l=> -[qs []]. unfold_leibniz.
   rewrite lookup_fmap fmap_Some_equiv=> -[s' [-> ->]] /Excl_included -> //.
 Qed.
 
@@ -35,7 +35,7 @@ Lemma own_ilft_auth_agree (I : gmap lft lft_names) κ γs :
     own ilft_name (◯ {[κ := to_agree γs]}) -∗ ⌜κ ∈ dom (gset _) I⌝.
 Proof.
   iIntros "HI Hκ". iDestruct (own_valid_2 with "HI Hκ")
-    as %[[? [Hl ?]]%singleton_included _]%auth_both_valid.
+    as %[[? [Hl ?]]%singleton_included_l _]%auth_both_valid.
   iPureIntro. apply elem_of_dom. unfold to_ilftUR in *. simplify_map_eq.
   destruct (fmap_Some_equiv_1 _ _ _ Hl) as (?&?&?). eauto.
 Qed.
@@ -46,7 +46,7 @@ Lemma own_alft_auth_agree (A : gmap atomic_lft (bool * Lat)) Λ bV :
 Proof.
   iIntros "HA HΛ".
   iDestruct (own_valid_2 with "HA HΛ") as %[HA _]%auth_both_valid.
-  iPureIntro. move: HA=> /singleton_included [qs []].
+  iPureIntro. move: HA=> /singleton_included_l [qs []].
   rewrite lookup_fmap fmap_Some_equiv=> -[bV' [-> ->]] /Some_included [EQ|/csum_included].
   - destruct bV as [[]?], bV' as [[]?]; (try by inversion EQ); do 2 f_equiv.
     + apply (inj Cinl), (inj2 pair) in EQ. naive_solver.
@@ -305,7 +305,7 @@ Proof.
   iSplit.
   - iIntros "H". iDestruct "H" as (V') "[#? H] ".
     (* FIXME : the Proper instance for singleton cannot be found automatically here. *)
-    rewrite (fin_maps.singleton_proper Λ _ (Cinl (_, to_latT V' ⋅ to_latT V'))); last first.
+    rewrite (fin_maps.singletonM_proper Λ _ (Cinl (_, to_latT V' ⋅ to_latT V'))); last first.
     { rewrite lat_op_join /= lat_join_idem //. } rewrite pair_op Cinl_op -op_singleton.
     iDestruct "H" as "[Hp Hq]". iSplitL "Hp"; auto.
   - iIntros "[Hp Hq]". iDestruct "Hp" as (Vp') "[#HVp' p]".
@@ -323,7 +323,7 @@ Lemma lft_tok_split_obj `{LatBottom Lat bot} q1 q2 κ :
 Proof.
   rewrite /lft_tok. rewrite -monPred_objectively_big_sepMS_entails -big_sepMS_sep.
   apply big_sepMS_mono=>// Λ ?. iStartProof (iProp _). iDestruct 1 as (V) "[#? H]".
-  rewrite (fin_maps.singleton_proper Λ _ (Cinl (_, to_latT V ⋅ to_latT bot))); last first.
+  rewrite (fin_maps.singletonM_proper Λ _ (Cinl (_, to_latT V ⋅ to_latT bot))); last first.
   { rewrite lat_op_join' right_id //. } rewrite pair_op Cinl_op -op_singleton.
   iDestruct "H" as "[Hp Hq]". iSplitL "Hp"; [by auto|]. iIntros (?). iExists bot. auto.
 Qed.