Commit 62436505 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 758d8d65 ea14f64d
Pipeline #1255 passed with stage
...@@ -713,7 +713,7 @@ Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4) ...@@ -713,7 +713,7 @@ Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
ltac:(iIntros { x1 x2 x3 x4 x5 x6 x7 x8 }). ltac:(iIntros { x1 x2 x3 x4 x5 x6 x7 x8 }).
(** * Assert *) (** * Assert *)
Tactic Notation "iAssert" constr(Q) "with" constr(Hs) "as" constr(pat) := Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
let H := iFresh in let H := iFresh in
let Hs := spec_pat.parse Hs in let Hs := spec_pat.parse Hs in
lazymatch Hs with lazymatch Hs with
...@@ -735,7 +735,7 @@ Tactic Notation "iAssert" constr(Q) "with" constr(Hs) "as" constr(pat) := ...@@ -735,7 +735,7 @@ Tactic Notation "iAssert" constr(Q) "with" constr(Hs) "as" constr(pat) :=
| ?pat => fail "iAssert: invalid pattern" pat | ?pat => fail "iAssert: invalid pattern" pat
end. end.
Tactic Notation "iAssert" constr(Q) "as" constr(pat) := Tactic Notation "iAssert" open_constr(Q) "as" constr(pat) :=
iAssert Q with "[]" as pat. iAssert Q with "[]" as pat.
(** * Rewrite *) (** * Rewrite *)
......
...@@ -53,7 +53,7 @@ Lemma Q_res_join γ : barrier_res γ Ψ1 ★ barrier_res γ Ψ2 ⊢ ▷ barrier_ ...@@ -53,7 +53,7 @@ Lemma Q_res_join γ : barrier_res γ Ψ1 ★ barrier_res γ Ψ2 ⊢ ▷ barrier_
Proof. Proof.
iIntros "[Hγ Hγ']"; iIntros "[Hγ Hγ']";
iDestruct "Hγ" as {x} "[#Hγ Hx]"; iDestruct "Hγ'" as {x'} "[#Hγ' Hx']". iDestruct "Hγ" as {x} "[#Hγ Hx]"; iDestruct "Hγ'" as {x'} "[#Hγ' Hx']".
iAssert ( (x x'):iProp)%I as "Hxx" . iAssert ( (x x'))%I as "Hxx" .
{ iCombine "Hγ" "Hγ'" as "Hγ2". iClear "Hγ Hγ'". { iCombine "Hγ" "Hγ'" as "Hγ2". iClear "Hγ Hγ'".
rewrite own_valid csum_validI /= agree_validI agree_equivI later_equivI /=. rewrite own_valid csum_validI /= agree_validI agree_equivI later_equivI /=.
rewrite -{2}[x]cFunctor_id -{2}[x']cFunctor_id. rewrite -{2}[x]cFunctor_id -{2}[x']cFunctor_id.
......
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