diff --git a/opam b/opam
index dbbeb23ff4b02daee0b0862cd6b2ecf083d00ef3..3830f0367eecdacae52365a84aa0fd646ed247db 100644
--- a/opam
+++ b/opam
@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-iris" { (= "dev.2019-02-05.0.eb921edd") | (= "dev") }
+  "coq-iris" { (= "dev.2019-02-20.0.8a8c1405") | (= "dev") }
 ]
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 14f35f7f7447c87309f24fff5b143b0d967bed43..0cd3d78d6e0ce93d6a18da066f66b51ef04d844c 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -102,7 +102,7 @@ Proof.
       iDestruct (own_bor_valid_2 with "Hinv Hf")
         as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_valid_discrete_2.
       by destruct INCL as [[=]|(? & ? & [=<-] &
-        [[_<-]%lookup_to_gmap_Some [[_ ?%(inj to_agree)]|[]%(exclusive_included _)]])].
+        [[_<-]%lookup_gset_to_gmap_Some [[_ ?%(inj to_agree)]|[]%(exclusive_included _)]])].
   - iMod (lft_dead_in_tok with "HA") as "[_ H†]". done.
     iDestruct (lft_tok_dead with "Htok H†") as "[]".
 Qed.
@@ -206,7 +206,7 @@ Proof.
       iDestruct (own_bor_valid_2 with "Hinv Hbor")
         as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_valid_discrete_2.
       by destruct INCL as [[=]|(? & ? & [=<-] &
-        [[_<-]%lookup_to_gmap_Some [[_?%(inj to_agree)]|[]%(exclusive_included _)]])].
+        [[_<-]%lookup_gset_to_gmap_Some [[_?%(inj to_agree)]|[]%(exclusive_included _)]])].
   - iMod (lft_dead_in_tok with "HA") as "[_ H†]". done.
     iDestruct (lft_tok_dead with "Htok H†") as "[]".
 Qed.
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 76788cdc9cba0ba72c1f8cc11b12f97b769db0d5..152af54861d89d70007a3f1b419d52cf61d62014 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -42,7 +42,7 @@ Proof.
   iApply fupd_trans. iApply fupd_mask_mono; first by apply union_subseteq_l.
   iMod ("Hvs" $! I with "[HI Halive Hbox Hbor] HP Hκ") as "(Hinv & HQ & Hcnt')".
   { rewrite lft_vs_inv_unfold. iFrame. rewrite /lft_bor_dead.
-    iExists (dom _ B), P. rewrite !to_gmap_dom -map_fmap_compose.
+    iExists (dom _ B), P. rewrite !gset_to_gmap_dom -map_fmap_compose.
     rewrite (map_fmap_ext _ ((1%Qp,) ∘ to_agree) B); last naive_solver.
     iFrame. }
   rewrite lft_vs_inv_unfold; iDestruct "Hinv" as "(?&HI&Halive)".
@@ -63,7 +63,7 @@ Lemma lfts_kill (A : gmap atomic_lft _) (I : gmap lft lft_names) (K K' : gset lf
     ={↑borN ∪ ↑inhN}=∗ Iinv K' ∗ [∗ set] κ ∈ K, lft_inv_dead κ.
 Proof.
   intros Iinv. revert K'.
-  induction (collection_wf K) as [K _ IH]=> K' HKK' HK HK'.
+  induction (set_wf K) as [K _ IH]=> K' HKK' HK HK'.
   iIntros "[HI Halive] HK".
   pose (Kalive := filter (lft_alive_in A) K).
   destruct (decide (Kalive = ∅)) as [HKalive|].
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index d5b45cfb6f1d5725eeb04dfa22c14144460edf9d..580275adacc4c2ef17c032ee5cbfabc043b6beb4 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -123,13 +123,13 @@ Section defs.
 
   Definition lft_bor_dead (κ : lft) : iProp Σ :=
      (∃ (B: gset slice_name) (Pb : iProp Σ),
-       own_bor κ (● to_gmap (1%Qp, to_agree Bor_in) B) ∗
-       box borN (to_gmap false B) Pb)%I.
+       own_bor κ (● gset_to_gmap (1%Qp, to_agree Bor_in) B) ∗
+       box borN (gset_to_gmap false B) Pb)%I.
 
    Definition lft_inh (κ : lft) (s : bool) (Pi : iProp Σ) : iProp Σ :=
      (∃ E : gset slice_name,
        own_inh κ (● GSet E) ∗
-       box inhN (to_gmap s E) Pi)%I.
+       box inhN (gset_to_gmap s E) Pi)%I.
 
    Definition lft_vs_inv_go (κ : lft) (lft_inv_alive : ∀ κ', κ' ⊂ κ → iProp Σ)
        (I : gmap lft lft_names) : iProp Σ :=
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index c00558ab0e1038044fe94f4f28bd590f6c0da31b..4dcbb159bd5afa1a17f96643d29e37bbd9fe120f 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -33,14 +33,14 @@ Proof.
   iAssert (own_cnt κ (◯ 0)) with "[Hcnt']" as "Hcnt'".
   { rewrite /own_cnt. iExists γs. by iFrame. }
   iAssert (∀ b, lft_inh κ b True)%I with "[Hinh]" as "Hinh".
-  { iIntros (b). rewrite /lft_inh. iExists ∅. rewrite to_gmap_empty.
+  { iIntros (b). rewrite /lft_inh. iExists ∅. rewrite gset_to_gmap_empty.
     iSplitL; [|iApply box_alloc]. rewrite /own_inh. iExists γs. by iFrame. }
   iAssert (lft_inv_dead κ ∧ lft_inv_alive κ)%I
     with "[-HA HI Hinv]" as "Hdeadandalive".
   { iSplit.
     - rewrite /lft_inv_dead. iExists True%I. iFrame "Hcnt".
       iSplitL "Hbor"; last by iApply "Hinh".
-      rewrite /lft_bor_dead. iExists ∅, True%I. rewrite !to_gmap_empty.
+      rewrite /lft_bor_dead. iExists ∅, True%I. rewrite !gset_to_gmap_empty.
       iSplitL "Hbor". iExists γs. by iFrame. iApply box_alloc.
     - rewrite lft_inv_alive_unfold. iExists True%I, True%I. iSplitL "Hbor".
       { rewrite /lft_bor_alive. iExists ∅.
@@ -85,9 +85,9 @@ Proof.
   iMod (own_bor_update with "HB●") as "[HB● H◯]".
   { eapply auth_update_alloc,
       (alloc_singleton_local_update _ _ (1%Qp, to_agree Bor_in)); last done.
-    by do 2 eapply lookup_to_gmap_None. }
+    by do 2 eapply lookup_gset_to_gmap_None. }
   rewrite /bor /raw_bor /idx_bor_own /=. iModIntro. iSplitR "H◯".
-  - iExists ({[γ]} ∪ B), (P ∗ Pinh)%I. rewrite !to_gmap_union_singleton. by iFrame.
+  - iExists ({[γ]} ∪ B), (P ∗ Pinh)%I. rewrite !gset_to_gmap_union_singleton. by iFrame.
   - iExists γ. iFrame. iExists P. rewrite -bi.iff_refl. eauto.
 Qed.
 
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 038aa8d1b47a93182ef95be688f661ec1e463381..25519cbb720858196889b39d116d03b387787c0b 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -448,10 +448,10 @@ Proof.
     as (γE) "(% & #Hslice & Hbox)".
   iMod (own_inh_update with "HE") as "[HE HE◯]".
   { by eapply auth_update_alloc, (gset_disj_alloc_empty_local_update _ {[γE]}),
-      disjoint_singleton_l, lookup_to_gmap_None. }
+      disjoint_singleton_l, lookup_gset_to_gmap_None. }
   iModIntro. iSplitL "Hbox HE".
   { iNext. rewrite /lft_inh. iExists ({[γE]} ∪ PE).
-    rewrite to_gmap_union_singleton. iFrame. }
+    rewrite gset_to_gmap_union_singleton. iFrame. }
   clear dependent PE. rewrite -(left_id_L ε op (◯ GSet {[γE]})).
   iDestruct "HE◯" as "[HE◯' HE◯]". iSplitL "HE◯'".
   { iIntros (I) "HI". iApply (own_inh_auth with "HI HE◯'"). }
@@ -462,11 +462,11 @@ Proof.
   { apply auth_update_dealloc, gset_disj_dealloc_local_update. }
   iMod (slice_delete_full _ _ true with "Hslice Hbox")
     as (Q'') "($ & #? & Hbox)"; first by solve_ndisj.
-  { rewrite lookup_to_gmap_Some. set_solver. }
+  { rewrite lookup_gset_to_gmap_Some. set_solver. }
   iModIntro. iExists Q''. iSplit; first done.
   iNext. rewrite /lft_inh. iExists (PE ∖ {[γE]}). iFrame "HE".
   rewrite {1}(union_difference_L {[ γE ]} PE); last set_solver.
-  rewrite to_gmap_union_singleton delete_insert // lookup_to_gmap_None.
+  rewrite gset_to_gmap_union_singleton delete_insert // lookup_gset_to_gmap_None.
   set_solver.
 Qed.
 
@@ -477,7 +477,7 @@ Proof.
   rewrite /lft_inh. iIntros (?) "[Hinh HQ]".
   iDestruct "Hinh" as (E') "[Hinh Hbox]".
   iMod (box_fill with "Hbox HQ") as "?"=>//.
-  rewrite fmap_to_gmap. iModIntro. iExists E'. by iFrame.
+  rewrite fmap_gset_to_gmap. iModIntro. iExists E'. by iFrame.
 Qed.
 
 (* View shifts *)
diff --git a/theories/typing/typing.v b/theories/typing/typing.v
index cdbc2552da4b4e7fd60dec80bceaaf673e24b10a..5b61f4b51d7c009e2f9915b01871d9645f76a8b0 100644
--- a/theories/typing/typing.v
+++ b/theories/typing/typing.v
@@ -5,5 +5,5 @@ From lrust.typing Require Export
   product_split borrow type_sum.
 
 (* Last, so that we make sure we shadow the defintion of delete for
-   collections coming from the prelude. *)
+   sets coming from the prelude. *)
 From lrust.lang Require Export new_delete.