From c17ab51c161c7a39f8ce90c592842d35452f8292 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 18 May 2021 10:31:01 +0200
Subject: [PATCH] coqdoc

---
 theories/decidable.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/decidable.v b/theories/decidable.v
index e33fd254..26e55cfe 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -136,12 +136,12 @@ Lemma bool_decide_eq_false_2 P `{!Decision P}: ¬P → bool_decide P = false.
 Proof. apply bool_decide_eq_false. Qed.
 
 (** The tactic [compute_done] solves the following kinds of goals:
-- Goals `P` where `Decidable P` can be derived.
-- Goals that compute to `True` or `x = x`.
+- Goals [P] where [Decidable P] can be derived.
+- Goals that compute to [True] or [x = x].
 
 The goal must be a ground term for this, i.e., not contain variables (that do
-not compute away). The goal is solved by using `vm_compute` and then using a
-trivial proof term (`I`/`eq_refl`). *)
+not compute away). The goal is solved by using [vm_compute] and then using a
+trivial proof term ([I]/[eq_refl]). *)
 Tactic Notation "compute_done" :=
   try apply (bool_decide_unpack _);
   vm_compute;
-- 
GitLab