Skip to content
Snippets Groups Projects
Commit e1308f3c authored by Ralf Jung's avatar Ralf Jung
Browse files

fix a FIXME

parent 7a3374e8
No related branches found
No related tags found
No related merge requests found
Pipeline #
Hide whitespace changes
Inline Side-by-side
theories/typing/cont_context.v
+ 1
− 2
View file @ e1308f3c
......@@ -64,7 +64,6 @@ Section cont_context.
constructor.
- iApply (HC1C2 with "LFT [H] HE * [%]"); last done.
iIntros "HE". iIntros (x') "%".
(* FIXME: If specialize follows by apply works, why does doing both in one apply loop? *)
iSpecialize ("H" with "HE"). iApply ("H" with "[%]"). by apply elem_of_cons; auto.
iApply ("H" with "HE * [%]"). by apply elem_of_cons; auto.
Qed.
End cont_context.
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