diff options
| -rw-r--r-- | tactics/class_tactics.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index c4ef32974c..1fadc164bf 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -160,11 +160,10 @@ let unify_resolve ~with_evars flags h diff = match diff with | Some (diff, ty) -> let () = assert (not h.hint_poly) in Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - let clenv = mk_clenv_from_n gl (Some diff) (h.hint_term, ty) in - let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in - let evd = Evd.merge_context_set Evd.univ_flexible evd h.hint_uctx in - let clenv = { clenv with evd = evd ; env = Proofview.Goal.env gl } in + let sigma, c = Hints.fresh_hint env sigma h in + let clenv = mk_clenv_from_env env sigma (Some diff) (c, ty) in Clenv.res_pf ~with_evars ~with_classes:false ~flags clenv end |