Commit eec05e0a authored by Ralf Jung's avatar Ralf Jung
Browse files

bump Iris; fix compatibility with latest std++

parent 4ee23161
...@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"] ...@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
depends: [ depends: [
"coq-iris" { (= "dev.2017-11-11.0") | (= "dev") } "coq-iris" { (= "dev.2017-11-14.0") | (= "dev") }
] ]
...@@ -97,7 +97,7 @@ Bind Scope val_scope with val. ...@@ -97,7 +97,7 @@ Bind Scope val_scope with val.
Definition of_val (v : val) : expr := Definition of_val (v : val) : expr :=
match v with match v with
| RecV f x e _ => Rec f x e | RecV f x e => Rec f x e
| LitV l => Lit l | LitV l => Lit l
end. end.
......
...@@ -26,7 +26,7 @@ Inductive expr := ...@@ -26,7 +26,7 @@ Inductive expr :=
Fixpoint to_expr (e : expr) : lang.expr := Fixpoint to_expr (e : expr) : lang.expr :=
match e with match e with
| Val v e' _ => e' | Val v e' _ => e'
| ClosedExpr e _ => e | ClosedExpr e => e
| Var x => lang.Var x | Var x => lang.Var x
| Lit l => lang.Lit l | Lit l => lang.Lit l
| Rec f xl e => lang.Rec f xl (to_expr e) | Rec f xl e => lang.Rec f xl (to_expr e)
...@@ -75,7 +75,7 @@ Ltac of_expr e := ...@@ -75,7 +75,7 @@ Ltac of_expr e :=
Fixpoint is_closed (X : list string) (e : expr) : bool := Fixpoint is_closed (X : list string) (e : expr) : bool :=
match e with match e with
| Val _ _ _ | ClosedExpr _ _ => true | Val _ _ _ | ClosedExpr _ => true
| Var x => bool_decide (x X) | Var x => bool_decide (x X)
| Lit _ => true | Lit _ => true
| Rec f xl e => is_closed (f :b: xl +b+ X) e | 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. ...@@ -120,7 +120,7 @@ Proof. intros [v ?]; exists v; eauto using to_val_Some. Qed.
Fixpoint subst (x : string) (es : expr) (e : expr) : expr := Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
match e with match e with
| Val v e H => Val v e H | 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 | Var y => if bool_decide (y = x) then es else Var y
| Lit l => Lit l | Lit l => Lit l
| Rec f xl e => | Rec f xl e =>
......
...@@ -83,22 +83,22 @@ Existing Instances tyl_wf_nil tyl_wf_cons. ...@@ -83,22 +83,22 @@ Existing Instances tyl_wf_nil tyl_wf_cons.
Fixpoint tyl_lfts `{typeG Σ} tyl {WF : TyWfLst tyl} : list lft := Fixpoint tyl_lfts `{typeG Σ} tyl {WF : TyWfLst tyl} : list lft :=
match WF with match WF with
| tyl_wf_nil => [] | tyl_wf_nil => []
| tyl_wf_cons ty [] _ _ => ty.(ty_lfts) | tyl_wf_cons ty [] => ty.(ty_lfts)
| tyl_wf_cons ty tyl _ _ => ty.(ty_lfts) ++ tyl.(tyl_lfts) | tyl_wf_cons ty tyl => ty.(ty_lfts) ++ tyl.(tyl_lfts)
end. end.
Fixpoint tyl_wf_E `{typeG Σ} tyl {WF : TyWfLst tyl} : elctx := Fixpoint tyl_wf_E `{typeG Σ} tyl {WF : TyWfLst tyl} : elctx :=
match WF with match WF with
| tyl_wf_nil => [] | tyl_wf_nil => []
| tyl_wf_cons ty [] _ _ => ty.(ty_wf_E) | 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 tyl => ty.(ty_wf_E) ++ tyl.(tyl_wf_E)
end. end.
Fixpoint tyl_outlives_E `{typeG Σ} tyl {WF : TyWfLst tyl} (κ : lft) : elctx := Fixpoint tyl_outlives_E `{typeG Σ} tyl {WF : TyWfLst tyl} (κ : lft) : elctx :=
match WF with match WF with
| tyl_wf_nil => [] | tyl_wf_nil => []
| tyl_wf_cons ty [] _ _ => ty.(ty_outlives_E) κ | 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 tyl => ty.(ty_outlives_E) κ ++ tyl.(tyl_outlives_E) κ
end. end.
Lemma tyl_outlives_E_elctx_sat `{typeG Σ} E L tyl {WF : TyWfLst tyl} α β : Lemma tyl_outlives_E_elctx_sat `{typeG Σ} E L tyl {WF : TyWfLst tyl} α β :
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment