From c52fd7fad39705dd428d8d4512e51a116a1e089e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Dani=C3=ABl=20Louwrink?= <daniel.louwrink@gmail.com>
Date: Fri, 1 May 2020 21:57:08 +0200
Subject: [PATCH] remove value restriction TODO

---
 theories/logrel/subtyping_rules.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index ef945aa..0c1b292 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -169,7 +169,6 @@ Section subtyping_rules.
     iApply (wp_wand with "H"). iIntros (v') "H Hle' !>".
     by iApply "Hle'".
   Qed.
-  (* TODO(COPY) TODO(VALUERES): Do the forall type former, once we have the value restriction *)
 
   Lemma lty_le_exist C1 C2 :
     ▷ (∀ A, C1 A <: C2 A) -∗
-- 
GitLab