diff --git a/theories/decidable.v b/theories/decidable.v
index 84aecad68f9991e67b7bb6b5392d0681f9f06030..e33fd2542d812cc1a680e01e552f255ae49dc6b2 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -139,12 +139,15 @@ Proof. apply bool_decide_eq_false. Qed.
 - 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`). *)
+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`). *)
 Tactic Notation "compute_done" :=
   try apply (bool_decide_unpack _);
   vm_compute;
   first [ exact I | exact eq_refl ].
+Tactic Notation "compute_by" tactic(tac) :=
+  tac; compute_done.
 
 (** Backwards compatibility notations. *)
 Notation bool_decide_true := bool_decide_eq_true_2.