diff --git a/theories/decidable.v b/theories/decidable.v
index e33fd2542d812cc1a680e01e552f255ae49dc6b2..26e55cfef5cd252e416d22799d3117e96c11c496 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;