From ec391f11e3e451110784c7f065e140321e42c0dc Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 28 Jul 2021 11:18:59 +0200
Subject: [PATCH] update dependencies

---
 opam                                    | 2 +-
 theories/examples/bit.v                 | 2 +-
 theories/experimental/helping/offers.v  | 2 +-
 theories/logic/adequacy.v               | 2 +-
 theories/logic/compatibility.v          | 2 +-
 theories/logic/derived.v                | 2 +-
 theories/logic/proofmode/tactics.v      | 2 +-
 theories/logic/rules.v                  | 2 +-
 theories/logic/spec_ra.v                | 2 +-
 theories/logic/spec_rules.v             | 2 +-
 theories/prelude/bijections.v           | 2 +-
 theories/reloc.v                        | 2 +-
 theories/tests/proofmode_tests.v        | 2 +-
 theories/tests/tp_tests.v               | 2 +-
 theories/typing/contextual_refinement.v | 2 +-
 theories/typing/fundamental.v           | 2 +-
 theories/typing/interp.v                | 2 +-
 theories/typing/soundness.v             | 2 +-
 18 files changed, 18 insertions(+), 18 deletions(-)

diff --git a/opam b/opam
index aa2413c..82259ad 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2021-06-18.0.366d607e") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2021-07-28.0.3424ace5") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]
diff --git a/theories/examples/bit.v b/theories/examples/bit.v
index aeb91c9..ffbf27b 100644
--- a/theories/examples/bit.v
+++ b/theories/examples/bit.v
@@ -1,6 +1,6 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** A simple bit module *)
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From reloc Require Import reloc.
 Set Default Proof Using "Type".
 
diff --git a/theories/experimental/helping/offers.v b/theories/experimental/helping/offers.v
index 0f86864..f54792c 100644
--- a/theories/experimental/helping/offers.v
+++ b/theories/experimental/helping/offers.v
@@ -1,7 +1,7 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Offers used to implement the stack with helping
 Based on the case study <https://iris-project.org/pdfs/2017-case-study-concurrent-stacks-with-helping.pdf> *)
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import excl.
 From reloc Require Export reloc.
 
diff --git a/theories/logic/adequacy.v b/theories/logic/adequacy.v
index d00cf9b..92c72bb 100644
--- a/theories/logic/adequacy.v
+++ b/theories/logic/adequacy.v
@@ -1,7 +1,7 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Adequacy statements for the refinement proposition *)
 From iris.algebra Require Import auth frac agree.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.heap_lang Require Export adequacy.
 From reloc.logic Require Export spec_ra model.
 
diff --git a/theories/logic/compatibility.v b/theories/logic/compatibility.v
index 3011969..31f9d31 100644
--- a/theories/logic/compatibility.v
+++ b/theories/logic/compatibility.v
@@ -1,6 +1,6 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Compataibility rules *)
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import list.
 From iris.program_logic Require Import ectx_lifting.
 From iris.heap_lang Require Import proofmode.
diff --git a/theories/logic/derived.v b/theories/logic/derived.v
index 6a93765..934eef8 100644
--- a/theories/logic/derived.v
+++ b/theories/logic/derived.v
@@ -1,6 +1,6 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Derived ReLoC rules *)
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import list.
 From iris.program_logic Require Import ectx_lifting.
 From iris.heap_lang Require Import proofmode.
diff --git a/theories/logic/proofmode/tactics.v b/theories/logic/proofmode/tactics.v
index 95661a1..8cfc9bc 100644
--- a/theories/logic/proofmode/tactics.v
+++ b/theories/logic/proofmode/tactics.v
@@ -6,7 +6,7 @@ From iris.proofmode Require Import
      reduction.
 From reloc.logic Require Import proofmode.spec_tactics.
 From reloc.logic Require Export model rules derived.
-From iris.proofmode Require Export tactics.
+From iris.proofmode Require Export proofmode.
 (* Set Default Proof Using "Type". *)
 
 (** * General-purpose tactics *)
diff --git a/theories/logic/rules.v b/theories/logic/rules.v
index 7bdb3f9..08b628d 100644
--- a/theories/logic/rules.v
+++ b/theories/logic/rules.v
@@ -1,6 +1,6 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Core ReLoC rules *)
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import list.
 From iris.program_logic Require Import ectx_lifting.
 From iris.heap_lang Require Import proofmode.
diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index bf0a45a..63bb374 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -3,7 +3,7 @@
 From iris.algebra Require Import auth excl gmap agree list frac.
 From iris.bi Require Export fractional.
 From iris.base_logic Require Export invariants.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.heap_lang Require Import lang primitive_laws.
 Import uPred.
 
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index 7cc744d..a02bc4e 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -1,7 +1,7 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Rules for updating the specification program. *)
 From iris.algebra Require Import auth excl frac agree gmap list.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.heap_lang Require Export lang notation tactics.
 From reloc.logic Require Export spec_ra.
 Import uPred.
diff --git a/theories/prelude/bijections.v b/theories/prelude/bijections.v
index a50655c..66d630c 100644
--- a/theories/prelude/bijections.v
+++ b/theories/prelude/bijections.v
@@ -4,7 +4,7 @@ Originally from: "A Logical Relation for Monadic Encapsulation of State: Proving
 by Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, Lars Birkedal *)
 From iris.algebra Require Import auth gset.
 From iris.base_logic Require Export invariants.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 Import uPred.
 
 Section PBij.
diff --git a/theories/reloc.v b/theories/reloc.v
index fed94d6..bab05af 100644
--- a/theories/reloc.v
+++ b/theories/reloc.v
@@ -1,5 +1,5 @@
 From iris.heap_lang Require Export lang notation proofmode.
-From iris.proofmode Require Export tactics.
+From iris.proofmode Require Export proofmode.
 From reloc.logic Require Export proofmode.tactics proofmode.spec_tactics model.
 From reloc.logic Require Export rules derived compatibility.
 From reloc.typing Require Export interp tactics soundness.
diff --git a/theories/tests/proofmode_tests.v b/theories/tests/proofmode_tests.v
index d8a8f0a..c1dd406 100644
--- a/theories/tests/proofmode_tests.v
+++ b/theories/tests/proofmode_tests.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From reloc.logic.proofmode Require Export spec_tactics tactics.
 From iris.heap_lang Require Import lang notation.
 
diff --git a/theories/tests/tp_tests.v b/theories/tests/tp_tests.v
index 93a20e2..0b7077e 100644
--- a/theories/tests/tp_tests.v
+++ b/theories/tests/tp_tests.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From reloc.logic Require Export spec_rules proofmode.spec_tactics.
 Set Default Proof Using "Type".
 Import lang.
diff --git a/theories/typing/contextual_refinement.v b/theories/typing/contextual_refinement.v
index 669627a..fb1e21f 100644
--- a/theories/typing/contextual_refinement.v
+++ b/theories/typing/contextual_refinement.v
@@ -3,7 +3,7 @@
 From Autosubst Require Import Autosubst.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import tactics.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From reloc.prelude Require Import lang_facts.
 From reloc.typing Require Export types interp fundamental.
 
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index c51d82c..46fcd4d 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -5,7 +5,7 @@ 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 iris.proofmode Require Export proofmode.
 
 Section fundamental.
   Context `{relocG Σ}.
diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index 06b3c58..c1347cd 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -2,7 +2,7 @@
 (** Interpretations for System F_mu_ref types *)
 From Autosubst Require Import Autosubst.
 From iris.algebra Require Export list.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From reloc.typing Require Export types.
 From reloc.logic Require Import model.
 From reloc.prelude Require Import properness asubst.
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 8be4cde..8093802 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -1,6 +1,6 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Logical relation is sound w.r.t. the contextual refinement. *)
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From reloc.logic Require Export adequacy.
 From reloc.typing Require Export contextual_refinement.
 
-- 
GitLab