Commit c73ba9c9 authored by Hai Dang's avatar Hai Dang
Browse files

Add a TODO

parent 5a791044
......@@ -4,6 +4,8 @@ From iris.proofmode Require Import proofmode classes.
Require Import iris.prelude.options.
(* TODO: currently unused *)
Section derived.
Context `{BiFUpd PROP} {TA TB : tele}.
Implicit Types
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment