expand compute_done to handle a few more kinds of goals

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.