diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v index 7b29d2216d6fce9156f02e2a83562f4539d83168..3cd6f64b465c10fd56c6642e4146e398f5f01dbc 100644 --- a/theories/typing/lib/cell.v +++ b/theories/typing/lib/cell.v @@ -82,9 +82,6 @@ End cell. Section typing. Context `{typeG Σ}. - (* TODO RJ: Consider setting this globally. *) - Arguments ty_own : simpl never. - (* Constructing a cell. *) Definition cell_new : val := funrec: <> ["x"] := return: ["x"].