diff --git a/opam b/opam
index b438a948ce4de320c914917ad0d3815ff83dbf2c..10a0bd29abae816db48cfcdcb238419baa061ceb 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.2017-11-11.0") | (= "dev") }
+  "coq-iris" { (= "dev.2017-11-14.0") | (= "dev") }
 ]
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index ff076bd1203608f29a711ea17ce1d976f107571f..5a750fb25e6a34f2b0148dbdc9495783fe02800a 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -97,7 +97,7 @@ Bind Scope val_scope with val.
 
 Definition of_val (v : val) : expr :=
   match v with
-  | RecV f x e _ => Rec f x e
+  | RecV f x e => Rec f x e
   | LitV l => Lit l
   end.
 
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index 91f722458b3295372bbc32fe8686062543d29bff..00edf34b15b93f4e087ba6bc6dcbbdae101c1da8 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -26,7 +26,7 @@ Inductive expr :=
 Fixpoint to_expr (e : expr) : lang.expr :=
   match e with
   | Val v e' _ => e'
-  | ClosedExpr e _ => e
+  | ClosedExpr e => e
   | Var x => lang.Var x
   | Lit l => lang.Lit l
   | Rec f xl e => lang.Rec f xl (to_expr e)
@@ -75,7 +75,7 @@ Ltac of_expr e :=
 
 Fixpoint is_closed (X : list string) (e : expr) : bool :=
   match e with
-  | Val _ _ _ | ClosedExpr _ _ => true
+  | Val _ _ _ | ClosedExpr _ => true
   | Var x => bool_decide (x ∈ X)
   | Lit _ => true
   | Rec f xl e => is_closed (f :b: xl +b+ X) e
@@ -120,7 +120,7 @@ Proof. intros [v ?]; exists v; eauto using to_val_Some. Qed.
 Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
   match e with
   | Val v e H => Val v e H
-  | ClosedExpr e H => @ClosedExpr e H
+  | @ClosedExpr e H => @ClosedExpr e H
   | Var y => if bool_decide (y = x) then es else Var y
   | Lit l => Lit l
   | Rec f xl e =>
diff --git a/theories/typing/type.v b/theories/typing/type.v
index a0f6cc6f10b61410c142d247c2c3193e5d6d3fda..5d2dd588fd04087d8af43fcf9b8cc35732185d81 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -83,22 +83,22 @@ Existing Instances tyl_wf_nil tyl_wf_cons.
 Fixpoint tyl_lfts `{typeG Σ} tyl {WF : TyWfLst tyl} : list lft :=
   match WF with
   | tyl_wf_nil => []
-  | tyl_wf_cons ty [] _ _ => ty.(ty_lfts)
-  | tyl_wf_cons ty tyl _ _ => ty.(ty_lfts) ++ tyl.(tyl_lfts)
+  | tyl_wf_cons ty [] => ty.(ty_lfts)
+  | tyl_wf_cons ty tyl => ty.(ty_lfts) ++ tyl.(tyl_lfts)
   end.
 
 Fixpoint tyl_wf_E `{typeG Σ} tyl {WF : TyWfLst tyl} : elctx :=
   match WF with
   | tyl_wf_nil => []
-  | tyl_wf_cons ty [] _ _ => ty.(ty_wf_E)
-  | tyl_wf_cons ty tyl _ _ => ty.(ty_wf_E) ++ tyl.(tyl_wf_E)
+  | tyl_wf_cons ty [] => ty.(ty_wf_E)
+  | tyl_wf_cons ty tyl => ty.(ty_wf_E) ++ tyl.(tyl_wf_E)
   end.
 
 Fixpoint tyl_outlives_E `{typeG Σ} tyl {WF : TyWfLst tyl} (κ : lft) : elctx :=
   match WF with
   | tyl_wf_nil => []
-  | tyl_wf_cons ty [] _ _ => ty.(ty_outlives_E) κ
-  | tyl_wf_cons ty tyl _ _ => ty.(ty_outlives_E) κ ++ tyl.(tyl_outlives_E) κ
+  | tyl_wf_cons ty [] => ty.(ty_outlives_E) κ
+  | tyl_wf_cons ty tyl => ty.(ty_outlives_E) κ ++ tyl.(tyl_outlives_E) κ
   end.
 
 Lemma tyl_outlives_E_elctx_sat `{typeG Σ} E L tyl {WF : TyWfLst tyl} α β :