From 498801d04837a1b1180ad91db5896e675f9f527b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 11 Feb 2020 19:34:20 +0100
Subject: [PATCH] Make compile with Coq 8.11.

---
 theories/examples/par.v       | 4 ++--
 theories/lib/lock.v           | 2 +-
 theories/prelude/ctx_subst.v  | 2 +-
 theories/typing/fundamental.v | 5 ++---
 4 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/theories/examples/par.v b/theories/examples/par.v
index b3abcde..da03015 100644
--- a/theories/examples/par.v
+++ b/theories/examples/par.v
@@ -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.
diff --git a/theories/lib/lock.v b/theories/lib/lock.v
index a246d56..f445991 100644
--- a/theories/lib/lock.v
+++ b/theories/lib/lock.v
@@ -1,5 +1,5 @@
-From reloc Require Export reloc.
 From iris.algebra Require Import excl.
+From reloc Require Export reloc.
 Set Default Proof Using "Type".
 
 
diff --git a/theories/prelude/ctx_subst.v b/theories/prelude/ctx_subst.v
index ce998bd..a8f2b67 100644
--- a/theories/prelude/ctx_subst.v
+++ b/theories/prelude/ctx_subst.v
@@ -1,6 +1,6 @@
+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)
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index 27e88df..0ef44e0 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -1,12 +1,11 @@
 (* 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".
-- 
GitLab