diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v index 9dc03accee77dcb2659ab7bebf3eae3229a9fb25..2f22221b24d75f9c5c39ae4eadd321f2b38d1799 100644 --- a/theories/typing/cont_context.v +++ b/theories/typing/cont_context.v @@ -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.