diff --git a/theories/typing/type.v b/theories/typing/type.v
index ef591793f0ba58ae1d144929564ebd3067ea6f72..5a8ba446351d633333ed21ff674f0c6beb9d8196 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),