Skip to content
Snippets Groups Projects
Commit 5734a780 authored by Hai Dang's avatar Hai Dang
Browse files

bump gpfsl

parent fb46b711
No related branches found
No related tags found
No related merge requests found
Pipeline #24122 failed
......@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
depends: [
"coq-gpfsl" { (= "dev.2020-02-03.1.4594b3d4") | (= "dev") }
"coq-gpfsl" { (= "dev.2020-02-11.1.5b5497be") | (= "dev") }
]
......@@ -80,8 +80,8 @@ Section refmut_functions.
iMod (bor_persistent with "LFT Hβδ Hα") as "[#Hβδ Hα]". done.
iMod (bor_sep with "LFT H") as "[_ H]". done.
iMod (bor_sep with "LFT H") as "[H _]". done.
unshelve (iMod (bor_fracture _ (λ q', (q * q').[ν])%I with "LFT H") as "H"=>//); try apply _; [| |].
{ split. by rewrite Qp_mult_1_r. apply _. } { done. }
unshelve (iMod (bor_fracture _ (λ q', (q * q').[ν])%I with "LFT H") as "H"=>//); try apply _; try done.
{ split. by rewrite Qp_mult_1_r. apply _. }
iDestruct (frac_bor_lft_incl _ _ q with "LFT H") as "#Hαν". iClear "H".
rewrite heap_mapsto_vec_cons. iMod (bor_sep with "LFT H↦") as "[H↦ _]". done.
iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hcloseα]". done.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment