diff --git a/theories/decidable.v b/theories/decidable.v
index 5471e7336bfe183e23c682b682dbb0b92417ebb5..84aecad68f9991e67b7bb6b5392d0681f9f06030 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -135,10 +135,16 @@ Proof. apply bool_decide_eq_false. Qed.
 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 a decidable goal by computing that it is
-true. *)
+(** 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`.
+
+The goal is solved by using `vm_compute` and then using a trivial proof term
+(`I`/`eq_refl`). *)
 Tactic Notation "compute_done" :=
-  apply (bool_decide_unpack _); vm_compute; exact I.
+  try apply (bool_decide_unpack _);
+  vm_compute;
+  first [ exact I | exact eq_refl ].
 
 (** Backwards compatibility notations. *)
 Notation bool_decide_true := bool_decide_eq_true_2.