From 64101a38eb83c50ad6dbd870588da4876b8293f6 Mon Sep 17 00:00:00 2001 From: Michael Sammler <noreply@sammler.me> Date: Mon, 14 Jun 2021 08:29:10 +0200 Subject: [PATCH] update iris --- refinedc.opam | 2 +- theories/lithium/base.v | 2 +- theories/typing/tyfold.v | 4 ++-- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/refinedc.opam b/refinedc.opam index 9d60a59c..9d44b760 100644 --- a/refinedc.opam +++ b/refinedc.opam @@ -17,7 +17,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/refinedc.git" depends: [ "coq" { (>= "8.12.0" & < "8.13~") } - "coq-iris" { (= "dev.2021-06-10.0.5d80dfef") | (= "dev") } + "coq-iris" { (= "dev.2021-06-12.0.3cb65333") | (= "dev") } "dune" {>= "2.7.0"} "cerberus" {= "~dev"} "cmdliner" {>= "1.0.4"} diff --git a/theories/lithium/base.v b/theories/lithium/base.v index bc321a2b..c2046a32 100644 --- a/theories/lithium/base.v +++ b/theories/lithium/base.v @@ -378,7 +378,7 @@ Proof. elim: l y => //=. Qed. Lemma list_lookup_length_default_last {A} (x : A) (l : list A) : (x :: l) !! length l = Some (default x (last l)). -Proof. elim: l x => //= a l IH x. rewrite IH. f_equal. destruct l => //. apply default_last_cons. Qed. +Proof. elim: l x => //= a l IH x. rewrite IH. f_equal. destruct l => //=. apply default_last_cons. Qed. Reserved Notation "'[∧' 'map]' k ↦ x ∈ m , P" diff --git a/theories/typing/tyfold.v b/theories/typing/tyfold.v index 80e60b0b..f058396a 100644 --- a/theories/typing/tyfold.v +++ b/theories/typing/tyfold.v @@ -36,7 +36,7 @@ Section tyfold. iDestruct "Htys" as "[H1 Hty2]". iDestruct "H1" as (l1 l2 ??) "H1". simplify_eq. iExists l2. rewrite tyexists_eq. iExists ls. rewrite tyexists_eq. iSplit => //. iSplitL "H1" => //=. rewrite /tyown_constraint. iSplit => //. iFrame. - iStopProof. f_equiv. destruct ls =>//. by apply default_last_cons. + iStopProof. f_equiv. destruct ls =>//=. by apply default_last_cons. Qed. Global Instance simplify_hyp_place_tyfold_optional_inst l β ls tys b: SimplifyHypPlace l β (ls @ tyfold tys b) (Some 50%N) := @@ -56,7 +56,7 @@ Section tyfold. iIntros "HT". iExists _. iFrame. iDestruct 1 as (l2 ls2 ->) "[Hl [% [Htys Hb]]]". iSplit => /=. by iPureIntro; f_equal. iFrame. iSplitR "Hb"; first by eauto with iFrame. - iStopProof. f_equiv. destruct ls2 =>//. by apply default_last_cons. + iStopProof. f_equiv. destruct ls2 =>//=. by apply default_last_cons. Qed. Global Instance simplify_goal_place_tyfold_cons_inst l β ls ty tys b: SimplifyGoalPlace l β (ls @ tyfold (ty :: tys) b) (Some 0%N) := -- GitLab