From 4875791a8298c4dc0f49bd4e0b1625ca64e9048a Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Thu, 19 Mar 2020 23:51:20 +0100 Subject: [PATCH] Fix Coqdoc. --- tests/proofmode.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/proofmode.v b/tests/proofmode.v index d5782bd97..e1c4ad813 100644 --- a/tests/proofmode.v +++ b/tests/proofmode.v @@ -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. -- GitLab