Commit 4875791a authored by Robbert Krebbers's avatar Robbert Krebbers

Fix Coqdoc.

parent d157edcc
......@@ -127,8 +127,8 @@ 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. *)
(** 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.
Proof. eexists. iIntros "?" (P). iAssumption. 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