Commit 676dd4ec authored by Ralf Jung's avatar Ralf Jung
Browse files

expand FIXME

parent a74b8077
......@@ -122,7 +122,7 @@ Proof. iExists {[ 1%positive ]}, ∅. auto. Qed.
Lemma test_iSpecialize_tc P : ( x y z : gset positive, P) - P.
Proof.
iIntros "H".
(* FIXME: this unshelve should not be needed. *)
(* FIXME: this [unshelve] and [apply _] should not be needed. *)
unshelve iSpecialize ("H" $! {[ 1%positive ]} ); try apply _. done.
Qed.
......
Markdown is supported
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