From eec05e0aa61e2e8346ab380d0930bbaca4cc1a31 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 14 Nov 2017 10:25:33 +0100
Subject: [PATCH] bump Iris; fix compatibility with latest std++

---
 opam                    |  2 +-
 theories/lang/lang.v    |  2 +-
 theories/lang/tactics.v |  6 +++---
 theories/typing/type.v  | 12 ++++++------
 4 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/opam b/opam
index b438a948..10a0bd29 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 ff076bd1..5a750fb2 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 91f72245..00edf34b 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 a0f6cc6f..5d2dd588 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} α β :
-- 
GitLab