Use `<:` (VMcast) for instances of `exact I` in lang/tactics.v

Title says it all. This way we get the benefits of vm_compute both during the proof and at Qed time. It brings the total compilation time down to ~7:40 from ~9:20 on the CI.

/cc @robbertkrebbers

theories/lang/tactics.v

@@ -172,7 +172,6 @@ Ltac solve_closed :=
   match goal with
   | |- Closed ?X ?e =>
      let e' := W.of_expr e in change (Closed X (W.to_expr e'));
-     (* apply W.is_closed_correct; vm_compute; exact I *)
      apply W.is_closed_correct; exact (I <: W.is_closed X e')
   end.
 Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
@@ -190,7 +189,6 @@ Ltac solve_to_val :=
   | |- is_Some (to_val ?e) =>
      let e' := W.of_expr e in change (is_Some (to_val (W.to_expr e')));
      apply W.to_val_is_Some, (bool_decide_unpack _);
-     (* vm_compute; exact I *)
      match goal with [|-Is_true (@bool_decide ?P ?dec)] =>
        exact (I <: Is_true (@bool_decide P dec))
      end
@@ -202,7 +200,6 @@ Ltac solve_atomic :=
   match goal with
   | |- Atomic ?s ?e =>
      let e' := W.of_expr e in change (Atomic s (W.to_expr e'));
-     (* apply W.is_atomic_correct; vm_compute; exact I *)
      apply W.is_atomic_correct; exact (I <: W.is_atomic e')
   end.
 Hint Extern 0 (Atomic _ _) => solve_atomic : typeclass_instances.