From 3c6d0d23667b2914549406467a7c038d24da73ae Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 11 Feb 2017 12:01:45 +0100
Subject: [PATCH] note a TODO

---
 theories/typing/unsafe/cell.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index 90efb807..1e6232ad 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -6,6 +6,10 @@ From lrust.typing Require Export type.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
+(* TODO: Some changes have recently landed in Rust adding
+   more operations to Cell for non-Copy types. We should make
+   sure we got them all covered. *)
+
 Section cell.
   Context `{typeG Σ}.
   Local Hint Extern 1000 (_ ⊆ _) => set_solver : ndisj.
-- 
GitLab