Commit 7d95a664 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris.

parent 30e470bc
Pipeline #20963 failed with stage
in 2 minutes and 51 seconds
......@@ -60,7 +60,7 @@ Section bi.
Inductive fracPred_entails (P1 P2 : fracPred) : Prop :=
{ fracPred_in_entails π : P1 π P2 π }.
Hint Immediate fracPred_in_entails.
Hint Immediate fracPred_in_entails : core.
Definition fracPred_embed_def (P : PROP) : fracPred := FracPred (λ _, P)%I.
Definition fracPred_embed_aux : seal (@fracPred_embed_def). by eexists. Qed.
......
......@@ -35,13 +35,13 @@ Ltac inv_head_step :=
inversion H; subst; clear H
end.
Local Hint Extern 0 (atomic _ _) => solve_atomic.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl.
Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _, _; simpl.
Local Hint Extern 0 (atomic _ _) => solve_atomic : core.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl : core.
Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _, _; simpl : core.
Local Hint Constructors head_step.
Local Hint Resolve alloc_fresh.
Local Hint Resolve to_of_val.
Local Hint Constructors head_step : core.
Local Hint Resolve alloc_fresh : core.
Local Hint Resolve to_of_val : core.
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
......
......@@ -168,10 +168,12 @@ Proof.
iExists ((π21 ? π22) / 2)%Qp, (Some ((π21 ? π22) / 2)%Qp). iFrame.
by rewrite /= !frac_op' Qp_div_2. }
iMod ("Hclose" with "[Hγauth Hp HP]") as "_"; first by eauto with iFrame.
iModIntro. iExists (π6 ? π5), ε; iSplit; first by rewrite left_id_L.
rewrite -union_difference_L //. iModIntro.
iExists (π6 ? π5), ε; iSplit; first by rewrite left_id_L.
eauto 10 with iFrame.
- iDestruct "Hcancel" as (π7 [π8|] ->) "[[-> Hγinv] Hγ] /="; try done.
iMod ("Hclose" with "[Hγinv]") as "_"; first by eauto.
rewrite -union_difference_L //. iModIntro.
iDestruct (own_valid_2 with "Hγauth Hγ") as %<-%frac_auth_agreeL.
iExists (π6 (π21 ? π22)), ε. eauto with iFrame.
Qed.
......
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