Commit 8c5c85c7 authored by Ralf Jung's avatar Ralf Jung
Browse files

bump Iris; fix for big-op move

parent b908d783
Pipeline #9125 passed with stage
in 14 minutes and 39 seconds
......@@ -6,5 +6,5 @@ install: [make "install"]
remove: ["rm" "-rf" "'%{lib}%/coq/user-contrib/fri"]
depends: [
"coq" { (>= "8.7.2") | (= "dev") }
"coq-iris" { (= "branch.gen_proofmode.2018-05-24.0.3bed085d") | (= "dev") }
"coq-iris" { (= "branch.gen_proofmode.2018-05-29.6.4417e093") | (= "dev") }
]
......@@ -204,7 +204,7 @@ Section lr.
rewrite /expr_equiv in pf.
specialize (pf ). rewrite /subst2typ fmap_empty in pf.
efeed pose proof pf as pf'; eauto; try done.
rewrite bi.big_sepM_empty right_id in pf' *.
rewrite big_sepM_empty right_id in pf' *.
intros ->; auto.
Qed.
......@@ -472,13 +472,13 @@ Tactic Notation "refine_unbind" constr(K) :=
⊣⊢ Φ s1 Φ s2 ([ map] zP S, Φ P)%I.
Proof.
intros Hneq Hl1 Hl2.
rewrite bi.big_sepM_insert; last first.
rewrite big_sepM_insert; last first.
- rewrite lookup_insert_ne; auto.
* move:Hl1. rewrite /subst2typ lookup_fmap.
case_eq (S !! x).
** intros s Heq. rewrite Heq. inversion 1.
** intros s Heq. auto.
- rewrite bi.big_sepM_insert; last first.
- rewrite big_sepM_insert; last first.
* move:Hl2. rewrite /subst2typ lookup_fmap.
case_eq (S !! y).
** intros s Heq. rewrite Heq. inversion 1.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment