From 9edc1b154b9360cb952b04867ed002561b6c5809 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 10 Feb 2017 12:13:26 +0100
Subject: [PATCH] leave a TODO

---
 theories/typing/type.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theories/typing/type.v b/theories/typing/type.v
index ef591793..5a8ba446 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -207,6 +207,7 @@ Bind Scope lrust_type_scope with type.
 Section ofe.
   Context `{typeG Σ}.
 
+  (* TODO: Use the ofe_iso infrastructure from Iris. *)
   Section def.
     Definition tuple_of_type (ty : type) : prodC (prodC _ _) _ :=
       (ty.(ty_size),
-- 
GitLab