diff --git a/theories/decidable.v b/theories/decidable.v
index 310eff9a1803fce53454c1195323f7cf206b0680..5471e7336bfe183e23c682b682dbb0b92417ebb5 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -135,6 +135,11 @@ 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. *)
+Tactic Notation "compute_done" :=
+  apply (bool_decide_unpack _); vm_compute; exact I.
+
 (** Backwards compatibility notations. *)
 Notation bool_decide_true := bool_decide_eq_true_2.
 Notation bool_decide_false := bool_decide_eq_false_2.
diff --git a/theories/list.v b/theories/list.v
index 4468f28b6433d8a1a662f84b571b6cda4401a66e..07bd5a5192897e4d5ce2055292719e15cba7ea1a 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -4537,7 +4537,7 @@ Ltac quote_Permutation :=
   end.
 Ltac solve_Permutation :=
   quote_Permutation; apply rlist.eval_Permutation;
-  apply (bool_decide_unpack _); by vm_compute.
+  compute_done.
 
 Ltac quote_submseteq :=
   match goal with
@@ -4549,7 +4549,7 @@ Ltac quote_submseteq :=
   end.
 Ltac solve_submseteq :=
   quote_submseteq; apply rlist.eval_submseteq;
-  apply (bool_decide_unpack _); by vm_compute.
+  compute_done.
 
 Ltac decompose_elem_of_list := repeat
   match goal with
diff --git a/theories/numbers.v b/theories/numbers.v
index bce80ceb10a9d27fde9eba02dcce9f5f5c746a80..5b520176f9c413354b84448525f7ea9afca15ee2 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -856,7 +856,7 @@ Lemma Qp_mul_1_r p : p * 1 = p.
 Proof. destruct p; apply Qp_to_Qc_inj_iff, Qcmult_1_r. Qed.
 
 Lemma Qp_1_1 : 1 + 1 = 2.
-Proof. apply (bool_decide_unpack _); by compute. Qed.
+Proof. compute_done. Qed.
 Lemma Qp_add_diag p : p + p = 2 * p.
 Proof. by rewrite <-Qp_1_1, Qp_mul_add_distr_r, !Qp_mul_1_l. Qed.
 
@@ -884,11 +884,11 @@ Proof.
   by rewrite Qp_mul_inv_l, Hp, Qp_mul_inv_l.
 Qed.
 Lemma Qp_inv_1 : /1 = 1.
-Proof. apply (bool_decide_unpack _); by compute. Qed.
+Proof. compute_done. Qed.
 Lemma Qp_inv_half_half : /2 + /2 = 1.
-Proof. apply (bool_decide_unpack _); by compute. Qed.
+Proof. compute_done. Qed.
 Lemma Qp_inv_quarter_quarter : /4 + /4 = /2.
-Proof. apply (bool_decide_unpack _); by compute. Qed.
+Proof. compute_done. Qed.
 
 Lemma Qp_div_diag p : p / p = 1.
 Proof. apply Qp_mul_inv_r. Qed.
@@ -917,13 +917,13 @@ Qed.
 Lemma Qp_div_2_mul p q : p / (2 * q) + p / (2 * q) = p / q.
 Proof. by rewrite <-Qp_div_add_distr, Qp_add_diag, Qp_div_mul_cancel_l. Qed.
 Lemma Qp_half_half : 1 / 2 + 1 / 2 = 1.
-Proof. apply (bool_decide_unpack _); by compute. Qed.
+Proof. compute_done. Qed.
 Lemma Qp_quarter_quarter : 1 / 4 + 1 / 4 = 1 / 2.
-Proof. apply (bool_decide_unpack _); by compute. Qed.
+Proof. compute_done. Qed.
 Lemma Qp_quarter_three_quarter : 1 / 4 + 3 / 4 = 1.
-Proof. apply (bool_decide_unpack _); by compute. Qed.
+Proof. compute_done. Qed.
 Lemma Qp_three_quarter_quarter : 3 / 4 + 1 / 4 = 1.
-Proof. apply (bool_decide_unpack _); by compute. Qed.
+Proof. compute_done. Qed.
 Global Instance Qp_div_inj_r p : Inj (=) (=) (Qp_div p).
 Proof. unfold Qp_div; apply _. Qed.
 Global Instance Qp_div_inj_l p : Inj (=) (=) (λ q, q / p)%Qp.
@@ -1218,7 +1218,7 @@ Lemma Qp_min_r_iff q p : q `min` p = p ↔ p ≤ q.
 Proof. rewrite (comm_L Qp_min q). apply Qp_min_l_iff. Qed.
 
 Lemma pos_to_Qp_1 : pos_to_Qp 1 = 1.
-Proof. apply (bool_decide_unpack _); by compute. Qed.
+Proof. compute_done. Qed.
 Lemma pos_to_Qp_inj n m : pos_to_Qp n = pos_to_Qp m → n = m.
 Proof. by injection 1. Qed.
 Lemma pos_to_Qp_inj_iff n m : pos_to_Qp n = pos_to_Qp m ↔ n = m.