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

---
 opam                                   | 2 +-
 theories/channel/proto.v               | 2 +-
 theories/channel/proto_model.v         | 2 +-
 theories/examples/list_rev.v           | 2 +-
 theories/examples/subprotocols.v       | 2 +-
 theories/examples/swap_mapper.v        | 2 +-
 theories/logrel/contexts.v             | 2 +-
 theories/logrel/examples/pair.v        | 2 +-
 theories/logrel/subtyping_rules.v      | 2 +-
 theories/logrel/term_typing_judgment.v | 2 +-
 theories/utils/contribution.v          | 2 +-
 11 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/opam b/opam
index 96e5496..3cde3f3 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2021-07-26.8.eb05e835") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2021-07-28.0.3424ace5") | (= "dev") }
 ]
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index b0b58bd..f0319c0 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -46,7 +46,7 @@ notions, such as contractiveness and non-expansiveness, after which the
 specifications of the message-passing primitives are defined in terms of the
 protocol connectives. *)
 From iris.algebra Require Import excl_auth.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.base_logic Require Export lib.iprop.
 From iris.base_logic Require Import lib.own.
 From iris.program_logic Require Import language.
diff --git a/theories/channel/proto_model.v b/theories/channel/proto_model.v
index 37c8fd0..2d5ddb4 100644
--- a/theories/channel/proto_model.v
+++ b/theories/channel/proto_model.v
@@ -34,7 +34,7 @@ The defined functions on the type [proto] are:
 - [proto_app], which appends two protocols [p1] and [p2], by substituting
   all terminations [END] in [p1] with [p2]. *)
 From iris.base_logic Require Import base_logic.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From actris.utils Require Import cofe_solver_2.
 Set Default Proof Using "Type".
 
diff --git a/theories/examples/list_rev.v b/theories/examples/list_rev.v
index 0f65fc9..2df2afe 100644
--- a/theories/examples/list_rev.v
+++ b/theories/examples/list_rev.v
@@ -1,5 +1,5 @@
 From actris.channel Require Import proofmode proto channel.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From actris.utils Require Import llist.
 
 Definition list_rev_service : val :=
diff --git a/theories/examples/subprotocols.v b/theories/examples/subprotocols.v
index c6842d4..7ab8a22 100644
--- a/theories/examples/subprotocols.v
+++ b/theories/examples/subprotocols.v
@@ -1,5 +1,5 @@
 From actris.channel Require Import proofmode proto channel.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 
 Section subprotocol_basics.
   Context `{heapGS Σ, chanG Σ}.
diff --git a/theories/examples/swap_mapper.v b/theories/examples/swap_mapper.v
index 42446ee..fb6b293 100644
--- a/theories/examples/swap_mapper.v
+++ b/theories/examples/swap_mapper.v
@@ -1,5 +1,5 @@
 From actris.channel Require Import proofmode proto channel.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From actris.utils Require Import llist.
 From iris.heap_lang Require Import notation.
 From actris.examples Require Import sort_fg.
diff --git a/theories/logrel/contexts.v b/theories/logrel/contexts.v
index fe0248a..1de8316 100644
--- a/theories/logrel/contexts.v
+++ b/theories/logrel/contexts.v
@@ -13,7 +13,7 @@ to the syntactic typing rules that are typically found in substructural type
 systems. *)
 From iris.algebra Require Export list.
 From iris.bi.lib Require Import core.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From actris.logrel Require Export term_types subtyping_rules.
 
 Inductive ctx_item Σ := CtxItem {
diff --git a/theories/logrel/examples/pair.v b/theories/logrel/examples/pair.v
index 6f7a6a5..4b8883c 100644
--- a/theories/logrel/examples/pair.v
+++ b/theories/logrel/examples/pair.v
@@ -8,7 +8,7 @@ can be assigned the type
 
 by exclusively using the semantic typing rules. *)
 From actris.logrel Require Export term_typing_rules session_typing_rules.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 
 Definition prog : expr := λ: "c", (recv "c", recv "c").
 
diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index 7ee3bfc..ef00bc4 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -2,7 +2,7 @@
 session types. *)
 From iris.bi.lib Require Import core.
 From iris.base_logic.lib Require Import invariants.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From actris.logrel Require Export subtyping term_types session_types.
 
 Section subtyping_rules.
diff --git a/theories/logrel/term_typing_judgment.v b/theories/logrel/term_typing_judgment.v
index 52fc272..ce5be82 100644
--- a/theories/logrel/term_typing_judgment.v
+++ b/theories/logrel/term_typing_judgment.v
@@ -9,7 +9,7 @@ semantically well-typed programs do not get stuck. *)
 From iris.heap_lang Require Import metatheory adequacy.
 From actris.logrel Require Export term_types.
 From actris.logrel Require Export contexts.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 
 (** The semantic typing judgment *)
 Definition ltyped `{!heapGS Σ}
diff --git a/theories/utils/contribution.v b/theories/utils/contribution.v
index 1a7d3af..6435034 100644
--- a/theories/utils/contribution.v
+++ b/theories/utils/contribution.v
@@ -16,7 +16,7 @@ later used in the protocol.
 To model this ghost theory construction, we use the camera
 [auth (option (csum (positive * A) (excl unit)))]. *)
 From iris.base_logic Require Export base_logic lib.iprop lib.own.
-From iris.proofmode Require Export tactics.
+From iris.proofmode Require Export proofmode.
 From iris.algebra Require Import excl auth csum gmultiset numbers.
 From iris.algebra Require Export local_updates.
 
-- 
GitLab