From 3e2ae1fc9de20523d7c446c1992aaf3d2a0c8bb0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 15 Feb 2017 21:24:48 +0100
Subject: [PATCH] Bump Iris and fix stuff.
---
opam.pins | 2 +-
theories/typing/bool.v | 2 +-
theories/typing/int.v | 2 +-
3 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/opam.pins b/opam.pins
index 9db15430..aa62552e 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq ea64fd148b56e1c38c08c2954e76bfa2e75b4db9
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 7b36d0e4c312b99b081f05b6575071b56bf12a55
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index a69d2e12..fd4c8c7b 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -13,7 +13,7 @@ Section bool.
| [ #(LitInt (0|1))] => True
| _ => False
end%I |}.
- Next Obligation. intros ? [|[[| |[|[]|]]|] []]; auto with I. Qed.
+ Next Obligation. intros ? [|[[| |[|[]|]]|] []]; auto. Qed.
Next Obligation. intros ? [|[[| |[|[]|]]|] []]; apply _. Qed.
Global Instance bool_send : Send bool.
diff --git a/theories/typing/int.v b/theories/typing/int.v
index e179a61b..d4d04fd1 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -12,7 +12,7 @@ Section int.
| [ #(LitInt z)] => True
| _ => False
end%I |}.
- Next Obligation. intros ? [|[[]|] []]; auto with I. Qed.
+ Next Obligation. intros ? [|[[]|] []]; auto. Qed.
Next Obligation. intros ? [|[[]|] []]; apply _. Qed.
Global Instance int_send : Send int.
--
GitLab