Commit eef6260f authored by Robbert Krebbers's avatar Robbert Krebbers

Add test case.

parent c9c90cf6
......@@ -239,6 +239,14 @@ Proof.
iFrame.
Qed.
Lemma test_iExists_unused : ( P : PROP, x : nat, P)%I.
Proof.
iExists _.
iExists 10.
iAssert emp%I as "H"; first done.
iExact "H".
Qed.
(* Check coercions *)
Lemma test_iExist_coercion (P : Z PROP) : ( x, P x) - x, P x.
Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). 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