From e1cfa2c42079bccb41a2eaba26f5af4b0251a8cd Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 22 Mar 2018 09:38:36 +0100
Subject: [PATCH] bump Iris; fix build
---
opam | 2 +-
theories/examples/list_lemmas.v | 4 ++--
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/opam b/opam
index 78b4fe3c..89b8bb9e 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/igps" ]
depends: [
- "coq-iris" { (= "branch.gen_proofmode.2018-03-21.0") | (= "dev") }
+ "coq-iris" { (= "branch.gen_proofmode.2018-03-21.3") | (= "dev") }
]
diff --git a/theories/examples/list_lemmas.v b/theories/examples/list_lemmas.v
index c55e8355..ec63bf57 100644
--- a/theories/examples/list_lemmas.v
+++ b/theories/examples/list_lemmas.v
@@ -1,4 +1,4 @@
-From iris.bi Require Import big_op.
+From iris.bi Require Import bi.
From igps Require Import infrastructure.
(* These lemmas probably belong somewhere higher. *)
@@ -44,4 +44,4 @@ Proof.
by erewrite nth_replicate.
Qed.
-End lemmas.
\ No newline at end of file
+End lemmas.
--
GitLab