Removing various compatibility layers of tactics.

1 files changed, 1 insertions, 0 deletions

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 9942e911a..e3f1c1ac2 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -461,6 +461,7 @@ let start_proof_com ?inference_hook kind thms hook =
   let thms = List.map (fun (sopt,(bl,t,guard)) ->
     let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
     let t', imps' = interp_type_evars_impls ~impls env evdref t in
+    let t' = EConstr.Unsafe.to_constr t' in
     let flags = all_and_fail_flags in
     let flags = { flags with use_hook = inference_hook } in
     evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref);