add exact_vm_cast

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.