Skip to content
Snippets Groups Projects
Commit 3c6d0d23 authored by Ralf Jung's avatar Ralf Jung
Browse files

note a TODO

parent 3bf41e48
No related branches found
No related tags found
No related merge requests found
...@@ -6,6 +6,10 @@ From lrust.typing Require Export type. ...@@ -6,6 +6,10 @@ From lrust.typing Require Export type.
From lrust.typing Require Import typing. From lrust.typing Require Import typing.
Set Default Proof Using "Type". 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. Section cell.
Context `{typeG Σ}. Context `{typeG Σ}.
Local Hint Extern 1000 (_ _) => set_solver : ndisj. Local Hint Extern 1000 (_ _) => set_solver : ndisj.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment