From 2943146f8b550cec72b792b67cedf18518ead67e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 27 Jan 2020 16:07:11 +0100
Subject: [PATCH] Bump Iris, and remove some stuff that's in Iris now.

---
 opam                          |  2 +-
 theories/prelude/properness.v | 52 -----------------------------------
 theories/typing/interp.v      | 11 +-------
 3 files changed, 2 insertions(+), 63 deletions(-)

diff --git a/opam b/opam
index 0a7b23a..1a22989 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
 depends: [
-  "coq-iris" { (= "dev.2019-11-21.0.e0d10c05") | (= "dev") }
+  "coq-iris" { (= "dev.2020-01-23.2.e2f65bbd") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/prelude/properness.v b/theories/prelude/properness.v
index e09f365..5a21ab5 100644
--- a/theories/prelude/properness.v
+++ b/theories/prelude/properness.v
@@ -37,55 +37,3 @@ Ltac properness :=
   | |- (_ ∗ _)%I ≡ (_ ∗ _)%I => apply sep_proper
   | |- (inv _ _)%I ≡ (inv _ _)%I => apply (contractive_proper _)
   end.
-
-Section big_opm.
-  Context `{Countable K} {A : ofeT}.
-  Context `{Monoid M o}.
-
-  Infix "`o`" := o (at level 50, left associativity).
-  Implicit Types m : gmap K A.
-  Implicit Types f g : K → A → M.
-
-  Global Instance big_opM_ne2 n `{Proper _ (dist n ==> dist n ==> dist n) o} :
-    Proper (pointwise_relation _ (dist n ==> dist n) ==> dist n ==> dist n)
-           (big_opM o (K:=K) (A:=A)).
-  Proof.
-    intros f g Hf m1.
-    induction m1 as [|i x m Hnone IH] using map_ind.
-    { intros m2 Hm2. rewrite big_opM_empty.
-      induction m2 as [|j y m2 ? IH2] using map_ind.
-      - by rewrite big_opM_empty.
-      - exfalso.
-        specialize (Hm2 j). revert Hm2.
-        rewrite lookup_insert lookup_empty /=. by inversion 1. }
-    intros m2 Hm2.
-    assert (is_Some (m2 !! i)) as [y Hy].
-    { specialize (Hm2 i). revert Hm2. rewrite lookup_insert=>Hm2.
-      destruct (m2 !! i); first naive_solver.
-      inversion Hm2. }
-    replace m2 with (<[i:=y]>(delete i m2)).
-    - rewrite !big_opM_insert // /=; last by apply lookup_delete.
-      f_equiv.
-      + apply Hf. specialize (Hm2 i). revert Hm2.
-        rewrite Hy lookup_insert //. by inversion 1.
-      + apply IH=> j.
-        destruct (decide (j = i)) as [->|?].
-        * by rewrite lookup_delete Hnone.
-        * rewrite lookup_delete_ne//. specialize (Hm2 j).
-          revert Hm2. by rewrite lookup_insert_ne.
-    - rewrite insert_delete insert_id //.
-  Qed.
-End big_opm.
-
-(** todo move somewhere *)
-Instance map_zip_with_ne {K} {A B C : ofeT} (f : A → B → C)
-  `{Countable K} `{!EqDecision K} n :
-  Proper (dist n ==> dist n ==> dist n) f →
-  Proper (dist n ==> dist n ==> dist n)
-    (@map_zip_with (gmap K) _ _ _ _ f).
-Proof.
-  intros Hf m1 m2 Hm2 m1' m2' Hm2' i.
-  rewrite !map_lookup_zip_with. f_equiv =>//.
-  intros x1 x2 Hx2. f_equiv =>//.
-  intros y1 y2 Hy2. repeat f_equiv =>//.
-Qed.
diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index 8db15c5..919b231 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -186,16 +186,7 @@ Section env_typed.
   Global Instance env_ltyped2_ne n :
     Proper (dist n ==> (=) ==> dist n) env_ltyped2.
   Proof.
-    intros Γ Γ' HΓ ? vvs ->.
-    rewrite /env_ltyped2 /big_sepM2.
-    f_equiv.
-    - f_equiv.
-      split;
-        intros Hvvs x; specialize (HΓ x); rewrite -(Hvvs x);
-          by apply (is_Some_ne n).
-    - apply big_opM_ne2; first apply _.
-      + by intros x A B ->.
-      + apply map_zip_with_ne=>//. apply _.
+    intros Γ Γ' HΓ ? vvs ->. apply big_sepM2_ne_2; [done..|solve_proper].
   Qed.
 
   Global Instance env_ltyped2_proper :
-- 
GitLab