Skip to content
Snippets Groups Projects
Commit 5592afd4 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump Iris and fix some stuff.

parent 24ea4cb1
No related branches found
No related tags found
No related merge requests found
Pipeline #
Hide whitespace changes
Inline Side-by-side
opam.pins
+ 1
− 1
View file @ 5592afd4
coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 7dec931b3ce0674c093a325275976aac96e9c8e6 coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 0429c257e3088cf77c8852a2cbeff2b02671b8b5
theories/typing/lib/rc.v
+ 1
− 4
View file @ 5592afd4
...@@ -154,10 +154,7 @@ Section rc. ...@@ -154,10 +154,7 @@ Section rc.
Lemma rc_subtype ty1 ty2 : Lemma rc_subtype ty1 ty2 :
type_incl ty1 ty2 -∗ type_incl (rc ty1) (rc ty2). type_incl ty1 ty2 -∗ type_incl (rc ty1) (rc ty2).
Proof. Proof.
iIntros "#Hincl". iPoseProof "Hincl" as "Hincl2". iIntros "#Hincl". iPoseProof "Hincl" as "(#Hsz & #Hoincl & #Hsincl)".
iDestruct "Hincl2" as "(#Hsz & #Hoincl & #Hsincl)".
(* FIXME: Would be nice to have an easier way to duplicate
destructed things. Maybe iPoseProof with a destruct pattern? *)
iSplit; first done. iSplit; iAlways. iSplit; first done. iSplit; iAlways.
- iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done. - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
iDestruct "Hvl" as "[(Hl & H† & Hc) | Hvl]". iDestruct "Hvl" as "[(Hl & H† & Hc) | Hvl]".
......
theories/typing/sum.v
+ 0
− 1
View file @ 5592afd4
...@@ -141,7 +141,6 @@ Section sum. ...@@ -141,7 +141,6 @@ Section sum.
{ iInduction Htyl as [|???? Hsub] "IH". { iInduction Htyl as [|???? Hsub] "IH".
{ iClear "∗". iIntros "!# _". done. } { iClear "∗". iIntros "!# _". done. }
iDestruct (Hsub with "HL") as "#Hsub". iDestruct ("IH" with "HL") as "{IH} #IH". iDestruct (Hsub with "HL") as "#Hsub". iDestruct ("IH" with "HL") as "{IH} #IH".
(* FIXME: WHy does the previous iDestruvt remove HL? *)
iAlways. iIntros "#HE". iDestruct ("Hsub" with "HE") as "(% & _ & _)". iAlways. iIntros "#HE". iDestruct ("Hsub" with "HE") as "(% & _ & _)".
iDestruct ("IH" with "HE") as %IH. iPureIntro. simpl. inversion_clear IH. by f_equal. } iDestruct ("IH" with "HE") as %IH. iPureIntro. simpl. inversion_clear IH. by f_equal. }
iDestruct (subtype_Forall2_llctx with "HL") as "#Htyl"; first done. iDestruct (subtype_Forall2_llctx with "HL") as "#Htyl"; first done.
......
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