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

Issue #55 of iris-coq has been fixed.

parent 6e29397b
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 @ 18ef7b44
coq-iris https://gitlab.mpi-sws.org/FP/iris-coq fb1712dd9da4d05ca2c919748633801934369d0d coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 5241c33d3013b81bb620b3cfd3cba1f2efdc5b2b
theories/typing/cont.v
+ 0
− 1
View file @ 18ef7b44
...@@ -34,7 +34,6 @@ Section typing. ...@@ -34,7 +34,6 @@ Section typing.
iIntros (args) "Htl HL HT". iApply wp_rec; try done. iIntros (args) "Htl HL HT". iApply wp_rec; try done.
{ rewrite Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. } { rewrite Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
{ by rewrite -(subst_v_eq (_ :: _) (RecV _ _ _ ::: _)). } { by rewrite -(subst_v_eq (_ :: _) (RecV _ _ _ ::: _)). }
(* FIXME: iNext here unfolds things in the context. *)
iNext. iApply (Hecont with "* HEAP LFT Htl HE HL [HC] HT"). iNext. iApply (Hecont with "* HEAP LFT Htl HE HL [HC] HT").
by iApply "IH". by iApply "IH".
Qed. Qed.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment