Commit 498801d0 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Make compile with Coq 8.11.

parent 2943146f
......@@ -216,7 +216,7 @@ Section rules.
iMod ("Hb" with "Hs Hi") as "Hb".
iApply (wp_wand with "Hb").
iIntros (bv). iDestruct 1 as (bv') "[Hi HB]". simpl.
wp_pures. wp_bind (join _).
wp_pures. wp_bind (spawn.join _).
iApply (join_spec with "Hdl").
iNext. iIntros (av). iDestruct 1 as (av') "[Hj HA]".
wp_pures.
......@@ -244,7 +244,7 @@ Section rules.
wp_pures. iExists (cv', dv')%V. simpl.
tp_pure i (InjR _). tp_store i.
tp_pure j (Lam _ _). tp_pure j _. simpl.
rewrite /join. tp_pure j (App _ #c2). simpl.
rewrite /spawn.join. tp_pure j (App _ #c2). simpl.
tp_load j. tp_case j. simpl.
tp_pure j (Lam _ _). tp_pure j (App _ cv'). simpl.
tp_pure j (Lam _ _). tp_pure j (App _ cv'). simpl.
......
From reloc Require Export reloc.
From iris.algebra Require Import excl.
From reloc Require Export reloc.
Set Default Proof Using "Type".
......
From stdpp Require Import base stringmap fin_sets fin_map_dom.
From iris.program_logic Require Export ectx_language ectxi_language.
From iris.heap_lang Require Export lang metatheory.
From stdpp Require Import base stringmap fin_sets fin_map_dom.
(** Substitution in the contexts *)
Fixpoint subst_map_ctx_item (es : stringmap val) (K : ectx_item)
......
(* ReLoC -- Relational logic for fine-grained concurrency *)
(** Compatibility lemmas for the logical relation *)
From Autosubst Require Import Autosubst.
From iris.heap_lang Require Import proofmode.
From reloc.logic Require Import model.
From reloc.logic Require Export rules derived compatibility proofmode.tactics.
From reloc.typing Require Export interp.
From iris.proofmode Require Export tactics.
From Autosubst Require Import Autosubst.
Section fundamental.
Context `{relocG Σ}.
......@@ -450,7 +449,7 @@ Section fundamental.
({Δ;Γ} e1 log e1' : ∃: τ) -
( τi : lrel Σ,
{τi::Δ;<[x:=τ]>(⤉Γ)}
e2 log e2' : (subst (ren (+1)%nat) τ2)) -
e2 log e2' : (Autosubst_Classes.subst (ren (+1)%nat) τ2)) -
{Δ;Γ} (unpack: x := e1 in e2) log (unpack: x := e1' in e2') : τ2.
Proof.
iIntros "IH1 IH2".
......
Markdown is supported
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