diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v index 90efb8071f51ede048594ca963c6b087b28cfaf1..1e6232ad52a95ac5e7a4febe5f06ad7d29e918dd 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.