From 42ccca26d324a5833096dad5f1d653bd19c669da Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 22 Feb 2018 10:22:24 +0100
Subject: [PATCH] Bump Iris, fix build.
---
opam | 2 +-
theories/lang/lib/memcpy.v | 1 -
theories/lang/lib/new_delete.v | 1 -
theories/lang/lib/swap.v | 1 -
theories/lang/proofmode.v | 1 -
5 files changed, 1 insertion(+), 5 deletions(-)
diff --git a/opam b/opam
index 94e2144e..32a6c2a3 100644
--- a/opam
+++ b/opam
@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
depends: [
- "coq-iris" { (= "dev.2018-02-20.1") | (= "dev") }
+ "coq-iris" { (= "dev.2018-02-21.1") | (= "dev") }
]
diff --git a/theories/lang/lib/memcpy.v b/theories/lang/lib/memcpy.v
index ecf05a02..7ec0166c 100644
--- a/theories/lang/lib/memcpy.v
+++ b/theories/lang/lib/memcpy.v
@@ -1,4 +1,3 @@
-From iris.base_logic.lib Require Import namespaces.
From lrust.lang Require Export notation.
From lrust.lang Require Import heap proofmode.
Set Default Proof Using "Type".
diff --git a/theories/lang/lib/new_delete.v b/theories/lang/lib/new_delete.v
index 35f95037..2320c69c 100644
--- a/theories/lang/lib/new_delete.v
+++ b/theories/lang/lib/new_delete.v
@@ -1,4 +1,3 @@
-From iris.base_logic.lib Require Import namespaces.
From lrust.lang Require Export notation.
From lrust.lang Require Import heap proofmode memcpy.
Set Default Proof Using "Type".
diff --git a/theories/lang/lib/swap.v b/theories/lang/lib/swap.v
index 38d96b17..86bd3206 100644
--- a/theories/lang/lib/swap.v
+++ b/theories/lang/lib/swap.v
@@ -1,4 +1,3 @@
-From iris.base_logic.lib Require Import namespaces.
From lrust.lang Require Export notation.
From lrust.lang Require Import heap proofmode.
Set Default Proof Using "Type".
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
index da0a116e..9c7eb813 100644
--- a/theories/lang/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -1,4 +1,3 @@
-From iris.base_logic Require Import namespaces.
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export tactics.
--
GitLab