From c85d0f7a5a37a2d856f2efb23674f8102b699e3c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 11 May 2021 14:03:59 +0200
Subject: [PATCH] expand compute_done to handle a few more kinds of goals

---
 theories/decidable.v | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/theories/decidable.v b/theories/decidable.v
index 5471e733..84aecad6 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.
-- 
GitLab