From e79c148fbe04fcb95c0a4ef4f98e0bc13c0c8bd9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 27 Apr 2017 15:34:08 +0200
Subject: [PATCH] simplification of ty_own is now fairly well-behaved, remove a
 TODO

---
 theories/typing/lib/cell.v | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 7b29d221..3cd6f64b 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"].
 
-- 
GitLab