From 46efc42728c4665d9111296adbb89643a9687bf5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 22 Aug 2017 17:24:55 +0200
Subject: [PATCH] update Iris
---
opam.pins | 2 +-
theories/typing/type.v | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/opam.pins b/opam.pins
index 9087d1ed..2c200453 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 398bae9d092b6568cf8d504ca98d8810979eea33
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 2e2c5c25aea886acc7d0925d435fe856ffa6ac14
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 2774efcd..9bcb847f 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -376,7 +376,7 @@ End type_contractive.
(* Tactic automation. *)
Ltac f_type_equiv :=
first [ ((eapply ty_size_type_dist || eapply ty_shr_type_dist || eapply ty_own_type_dist); try reflexivity) |
- match goal with | |- @dist_later ?A ?n ?x ?y =>
+ match goal with | |- @dist_later ?A _ ?n ?x ?y =>
destruct n as [|n]; [exact I|change (@dist A _ n x y)]
end ].
Ltac solve_type_proper :=
--
GitLab