From 33e935c99c0f1403193e6a16d6e168f696548fbc Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 1 Mar 2018 14:00:34 +0100
Subject: [PATCH] add exact_vm_cast

---
 theories/tactics.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/tactics.v b/theories/tactics.v
index 8492287..2a019db 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -77,6 +77,13 @@ Ltac done_if b :=
   | false => idtac
   end.
 
+(** A version of [exact] that inserts a vm_cast into the term. On the pro side,
+this means that vm_compute will be used at Qed time to check the cast. However,
+this also embeds a copy of the current goal into the proof term, resulting in a
+larger term. The difference to ssreflect's [exact<:] is that conversion checking
+is also performed immediately, whereas [exact<:] only checks at Qed time. *)
+Ltac exact_vm_cast t := match goal with |- ?P => exact (t <: P) end.
+
 (** Aliases for trans and etrans that are easier to type *)
 Tactic Notation "trans" constr(A) := transitivity A.
 Tactic Notation "etrans" := etransitivity.
-- 
GitLab