leave a TODO

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),

[Robbert Krebbers]

That's on my list, and that is why I actually created that the ofe_iso stuff in Iris.

Besides, when redoing this, we should make sure that all these definitions are sealed. I noticed that at some places Coq is unfolding them, making it very slow.

[Ralf Jung]

Notice that I want to re-do the entire handling of recursive types at some point, and stop using the hack involving type-level later in the definition here.