From 14ccc4c8c81b58373639a23d219aca41d4ad7c9a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 13 May 2021 16:11:44 +0200
Subject: [PATCH] add compute_by

---
 theories/decidable.v | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

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