From 87413b9602d00bdb64ae3591f887606cb9eaa7c2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 9 Feb 2017 17:29:34 +0100
Subject: [PATCH] Remove obsolete TODO.
---
theories/typing/type.v | 1 -
1 file changed, 1 deletion(-)
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 1ef9e656..37f2f538 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -341,7 +341,6 @@ Section subtyping.
Lemma type_incl_trans ty1 ty2 ty3 :
type_incl ty1 ty2 -∗ type_incl ty2 ty3 -∗ type_incl ty1 ty3.
Proof.
- (* TODO: this iIntros takes suspiciously long. *)
iIntros "(% & #Ho12 & #Hs12) (% & #Ho23 & #Hs23)".
iSplit; first (iPureIntro; etrans; done).
iSplit; iAlways; iIntros.
--
GitLab