From 8e6ed558860740ec5e763cac14e7417dfb1f1fa8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 17 Jul 2020 13:46:50 +0200
Subject: Further code simplification in typeclass resolution tactic.

---
 tactics/class_tactics.ml | 7 +++----
 1 file 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
 
-- 
cgit v1.2.3