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

simplification of ty_own is now fairly well-behaved, remove a TODO

parent f949325c
No related branches found
No related tags found
No related merge requests found
Pipeline #
......@@ -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"].
......
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