diff --git a/theories/tactics.v b/theories/tactics.v
index 849228769060084f48401cb9b77ef3eeb181635a..2a019dbdc8d0aed65a00b96c0526b2c5a25dc098 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.