From 02dd160233adc784eac732d97a88356d1f0eaf9b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 25 Nov 2016 18:34:53 +0100
Subject: Removing various compatibility layers of tactics.

---
 stm/lemmas.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'stm')

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 9942e911ab..e3f1c1ac28 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);
-- 
cgit v1.2.3