Commit 2c980e72 authored by Robbert Krebbers's avatar Robbert Krebbers

Add test.

parent a42f1b54
......@@ -109,6 +109,10 @@ Lemma test_very_fast_iIntros P :
x y : nat, ( x = y P - P)%I.
Proof. by iIntros. Qed.
Definition tc_opaque_test : PROP := tc_opaque ( x : nat, x = x )%I.
Lemma test_iIntros_tc_opaque : tc_opaque_test.
Proof. by iIntros (x). Qed.
(** Prior to 0b84351c this used to loop, now `iAssumption` instantiates `R` with
`False` and performs false elimination. *)
Lemma test_iAssumption_evar_ex_false : R, R P, P.
......
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