diff --git a/theories/decidable.v b/theories/decidable.v
index 89b74b2e74aec5081614b8d613007a5ffedc3d99..64befc94428f4fb0060c141dc32668b2ba27f6ad 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -135,6 +135,20 @@ 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 the following kinds of goals:
+- 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]). *)
+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.
 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 23675b3b1533e47573e6edd5cc1b7b50caeb4fce..f3563fb485bacea9861683df2a1fbe9674db70bd 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -865,7 +865,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.
 
@@ -893,11 +893,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.
@@ -926,13 +926,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.
@@ -1227,7 +1227,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.