diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/lemmas.ml | 1 |
1 files changed, 1 insertions, 0 deletions
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); |