From e1308f3c67f064ee48ea9b5eec33c1332d41c42a Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Fri, 16 Dec 2016 08:37:10 +0100
Subject: [PATCH] fix a FIXME
---
theories/typing/cont_context.v | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index 9dc03acc..2f22221b 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.
--
GitLab