diff --git a/.gitignore b/.gitignore
index db187c816131a6b7827c84d29602c93513cb3c4f..23ef4c4425ad44d7a61fc693ab762e57f0981f5e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,7 +1,10 @@
 *.vo
 *.vio
 *.v.d
+*.vos
+*.vok
 .coqdeps.d
+.Makefile.coq.d
 *.glob
 *.cache
 *.aux
diff --git a/opam b/opam
index 8da289fd4cb64e49470ad7a6beb5efafeecc6f6a..298e0e9706b1cecaa28c290cbfa9d8753fc09958 100644
--- a/opam
+++ b/opam
@@ -14,7 +14,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2020-01-17.1.5088d5b0") | (= "dev") }
+  "coq-iris" { (= "dev.2020-02-12.1.db3bebcd") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/typing/examples/nonlexical.v b/theories/typing/examples/nonlexical.v
index 2666af36b38fb2ea633de568ec99da47b5bde83b..372faee59c50774e751dab40420cdd2da0b48f59 100644
--- a/theories/typing/examples/nonlexical.v
+++ b/theories/typing/examples/nonlexical.v
@@ -88,7 +88,7 @@ Section non_lexical.
       iApply type_endlft.
       iApply (type_cont [_] [ϝ ⊑ₗ []]
             (λ r, [o ◁ box (Π[uninit 1;uninit 1]); map ◁ box (uninit 1);
-                   key ◁ box K; r!!!0 ◁ box (&uniq{m} V)])).
+                   key ◁ box K; (r!!!0%fin:val) ◁ box (&uniq{m} V)])).
       { iIntros (k). simpl_subst.
         iApply type_case_own;
           [solve_typing| constructor; [|constructor; [|constructor]]; left].
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 6fe52645302722f1c775e52b2f1b0124fb537409..53cabf07c0fbe0fdc4af5c019bd3bf69908254b1 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -24,7 +24,7 @@ Section fn.
          ⌜vl = [@RecV fb (kb::xb) e H]⌝ ∗ ⌜length xb = n⌝ ∗
          ▷ ∀ (x : A) (ϝ : lft) (k : val) (xl : vec val (length xb)),
             □ typed_body ((fp x).(fp_E)  ϝ) [ϝ ⊑ₗ []]
-                         [k◁cont([ϝ ⊑ₗ []], λ v : vec _ 1, [v!!!0 ◁ box (fp x).(fp_ty)])]
+                         [k◁cont([ϝ ⊑ₗ []], λ v : vec _ 1, [(v!!!0%fin:val) ◁ box (fp x).(fp_ty)])]
                          (zip_with (TCtx_hasty ∘ of_val) xl
                                    (box <$> (vec_to_list (fp x).(fp_tys))))
                          (subst_v (fb::kb::xb) (RecV fb (kb::xb) e:::k:::xl) e))%I |}.
@@ -318,7 +318,7 @@ Section typing.
                    {A} (fp : A → fn_params (length ps)) (k : val) x :
     Forall (lctx_lft_alive E L) κs →
     (∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ₑ κ) <$> κs) ++ E) L ((fp x).(fp_E) ϝ)) →
-    typed_body E L [k ◁cont(L, λ v : vec _ 1, (v!!!0 ◁ box (fp x).(fp_ty)) :: T)]
+    typed_body E L [k ◁cont(L, λ v : vec _ 1, ((v!!!0%fin:val) ◁ box (fp x).(fp_ty)) :: T)]
                ((p ◁ fn fp) ::
                 zip_with TCtx_hasty ps (box <$> vec_to_list (fp x).(fp_tys)) ++
                 T)
@@ -366,7 +366,7 @@ Section typing.
     typed_body E L C T (letcall: b := p ps in e).
   Proof.
     iIntros (?? Hpsc ????) "He".
-    iApply (type_cont_norec [_] _ (λ r, (r!!!0 ◁ box (fp x).(fp_ty)) :: T')).
+    iApply (type_cont_norec [_] _ (λ r, ((r!!!0%fin:val) ◁ box (fp x).(fp_ty)) :: T')).
     - (* TODO : make [solve_closed] work here. *)
       eapply is_closed_weaken; first done. set_solver+.
     - (* TODO : make [solve_closed] work here. *)
@@ -395,7 +395,7 @@ Section typing.
     n = length argsb →
     □ (∀ x ϝ (f : val) k (args : vec val (length argsb)),
           typed_body ((fp x).(fp_E) ϝ) [ϝ ⊑ₗ []]
-                     [k ◁cont([ϝ ⊑ₗ []], λ v : vec _ 1, [v!!!0 ◁ box (fp x).(fp_ty)])]
+                     [k ◁cont([ϝ ⊑ₗ []], λ v : vec _ 1, [(v!!!0%fin:val) ◁ box (fp x).(fp_ty)])]
                      ((f ◁ fn fp) ::
                         zip_with (TCtx_hasty ∘ of_val) args
                                  (box <$> vec_to_list (fp x).(fp_tys)) ++ T)
@@ -418,7 +418,7 @@ Section typing.
     n = length argsb →
     □ (∀ x ϝ k (args : vec val (length argsb)),
         typed_body ((fp x).(fp_E) ϝ) [ϝ ⊑ₗ []]
-                   [k ◁cont([ϝ ⊑ₗ []], λ v : vec _ 1, [v!!!0 ◁ box (fp x).(fp_ty)])]
+                   [k ◁cont([ϝ ⊑ₗ []], λ v : vec _ 1, [(v!!!0%fin:val) ◁ box (fp x).(fp_ty)])]
                    (zip_with (TCtx_hasty ∘ of_val) args
                              (box <$> vec_to_list (fp x).(fp_tys)) ++ T)
                    (subst_v (BNamed "return" :: argsb) (k ::: args) e)) -∗
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 964ecea96fc47cdbd95eea30cf5a11f59f3123cc..a53ac9e45213ffdb5a336c9643db1616b0eb3d99 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -258,7 +258,7 @@ Section rwlock_functions.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply (type_cont [_] [ϝ ⊑ₗ []] (λ r, [x ◁ box (&shr{α}(rwlock ty));
-                                        r!!!0 ◁ box (option (rwlockwriteguard α ty))]));
+                                        (r!!!0%fin:val) ◁ box (option (rwlockwriteguard α ty))]));
       [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg=>r];
       simpl_subst; last first.
     { iApply type_delete; [solve_typing..|]. iApply type_jump; solve_typing. }