From 85e56b4c25071f048624ffbe7f7891f6f1534127 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 2 Jul 2020 15:34:27 +0200
Subject: Inline Class_tactics.clenv_of_prods.

It was unnecessarily obfuscated.
---
 tactics/class_tactics.ml | 37 ++++++++++++++-----------------------
 1 file changed, 14 insertions(+), 23 deletions(-)

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 63cafbf76d..94c5ca38fb 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -211,32 +211,23 @@ let unify_resolve_refine flags gl clenv =
 (** Dealing with goals of the form A -> B and hints of the form
   C -> A -> B.
 *)
-let clenv_of_prods nprods h gl =
-  let { hint_term = c; hint_clnv = clenv; hint_poly = poly } = h in
-  if poly || Int.equal nprods 0 then Some (None, clenv)
-  else
-    let sigma = Tacmach.New.project gl in
-    let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma c in
-    let diff = nb_prod sigma ty - nprods in
-    if (>=) diff 0 then
-      (* Was Some clenv... *)
-      Some (Some diff,
-            mk_clenv_from_n gl (Some diff) (c,ty))
-    else None
-
 let with_prods nprods h f =
   if get_typeclasses_limit_intros () then
     Proofview.Goal.enter begin fun gl ->
-      try match clenv_of_prods nprods h gl with
-          | None ->
-            let info = Exninfo.reify () in
-            Tacticals.New.tclZEROMSG ~info (str"Not enough premisses")
-          | Some (diff, clenv') ->
-            let h = { h with hint_clnv = clenv' } in
-            f gl (h, diff)
-      with e when CErrors.noncritical e ->
-        let e, info = Exninfo.capture e in
-        Proofview.tclZERO ~info e end
+      let { hint_term = c; hint_clnv = clenv; hint_poly = poly } = h in
+      if poly || Int.equal nprods 0 then
+        f gl (h, None)
+      else
+        let sigma = Tacmach.New.project gl in
+        let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma c in
+        let diff = nb_prod sigma ty - nprods in
+        if (>=) diff 0 then
+          (* Was Some clenv... *)
+          let clenv = mk_clenv_from_n gl (Some diff) (c,ty) in
+          let h = { h with hint_clnv = clenv } in
+          f gl (h, Some diff)
+        else Tacticals.New.tclZEROMSG (str"Not enough premisses")
+    end
   else Proofview.Goal.enter
          begin fun gl ->
          if Int.equal nprods 0 then f gl (h, None)
-- 
cgit v1.2.3


From e52a8a898352f55fb544e2b563c81fd1247c8130 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 2 Jul 2020 15:38:20 +0200
Subject: Perfom an goal enter in the relevant class tactics instead of
 outside.

---
 tactics/class_tactics.ml | 32 +++++++++++++++++---------------
 1 file changed, 17 insertions(+), 15 deletions(-)

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 94c5ca38fb..e28ce1b85a 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -161,19 +161,20 @@ let e_give_exact flags h =
   Clenv.unify ~flags t1 <*> exact_no_check c
   end
 
-let unify_e_resolve flags = begin fun gls (h, _) ->
+let unify_e_resolve flags (h, _) = Proofview.Goal.enter begin fun gls ->
   let clenv', c = connect_hint_clenv h gls in
   Clenv.res_pf ~with_evars:true ~with_classes:false ~flags clenv'
   end
 
-let unify_resolve flags = begin fun gls (h, _) ->
+let unify_resolve flags (h, _) = Proofview.Goal.enter begin fun gls ->
   let clenv', _ = connect_hint_clenv h gls in
   Clenv.res_pf ~with_evars:false ~with_classes:false ~flags clenv'
   end
 
 (** Application of a lemma using [refine] instead of the old [w_unify] *)
-let unify_resolve_refine flags gls (h, n) =
-  let { hint_term = c; hint_type = t; hint_uctx = ctx; hint_clnv = clenv } = h in
+let unify_resolve_refine flags (h, n) =
+  Proofview.Goal.enter begin fun gls ->
+  let { hint_term = c; hint_type = t; hint_uctx = ctx } = h in
   let open Clenv in
   let env = Proofview.Goal.env gls in
   let concl = Proofview.Goal.concl gls in
@@ -195,10 +196,11 @@ let unify_resolve_refine flags gls (h, n) =
                     ~flags:(default_flags_of flags.core_unify_flags.modulo_delta)
                               env sigma' cl.cl_concl concl)
       in (sigma', term) end
+  end
 
-let unify_resolve_refine flags gl clenv =
+let unify_resolve_refine flags clenv =
   Proofview.tclORELSE
-    (unify_resolve_refine flags gl clenv)
+    (unify_resolve_refine flags clenv)
     (fun (exn,info) ->
       match exn with
       | Evarconv.UnableToUnify _ ->
@@ -216,7 +218,7 @@ let with_prods nprods h f =
     Proofview.Goal.enter begin fun gl ->
       let { hint_term = c; hint_clnv = clenv; hint_poly = poly } = h in
       if poly || Int.equal nprods 0 then
-        f gl (h, None)
+        f (h, None)
       else
         let sigma = Tacmach.New.project gl in
         let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma c in
@@ -225,12 +227,12 @@ let with_prods nprods h f =
           (* Was Some clenv... *)
           let clenv = mk_clenv_from_n gl (Some diff) (c,ty) in
           let h = { h with hint_clnv = clenv } in
-          f gl (h, Some diff)
+          f (h, Some diff)
         else Tacticals.New.tclZEROMSG (str"Not enough premisses")
     end
   else Proofview.Goal.enter
          begin fun gl ->
-         if Int.equal nprods 0 then f gl (h, None)
+         if Int.equal nprods 0 then f (h, None)
          else Tacticals.New.tclZEROMSG (str"Not enough premisses") end
 
 let matches_pattern concl pat =
@@ -338,9 +340,9 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
            if get_typeclasses_filtered_unification () then
              let tac =
                with_prods nprods h
-                          (fun gl clenv ->
+                          (fun clenv ->
                              matches_pattern concl p <*>
-                               unify_resolve_refine flags gl clenv)
+                               unify_resolve_refine flags clenv)
              in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
            else
              let tac =
@@ -350,9 +352,9 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
         | ERes_pf h ->
            if get_typeclasses_filtered_unification () then
              let tac = (with_prods nprods h
-                  (fun gl clenv ->
+                  (fun clenv ->
                              matches_pattern concl p <*>
-                             unify_resolve_refine flags gl clenv)) in
+                             unify_resolve_refine flags clenv)) in
              Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
            else
              let tac =
@@ -364,7 +366,7 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
              let tac =
                matches_pattern concl p <*>
                  Proofview.Goal.enter
-                   (fun gl -> unify_resolve_refine flags gl (h, None)) in
+                   (fun gl -> unify_resolve_refine flags (h, None)) in
              Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
            else
              e_give_exact flags h
@@ -1227,7 +1229,7 @@ let autoapply c i =
   let cty = Tacmach.New.pf_get_type_of gl c in
   let ce = mk_clenv_from gl (c,cty) in
   let h = { hint_term = c; hint_type = cty; hint_uctx = Univ.ContextSet.empty; hint_clnv = ce; hint_poly = false } in
-    unify_e_resolve flags gl (h, 0) <*>
+    unify_e_resolve flags (h, 0) <*>
       Proofview.tclEVARMAP >>= (fun sigma ->
       let sigma = Typeclasses.make_unresolvables
           (fun ev -> Typeclasses.all_goals ev (Lazy.from_val (snd (Evd.find sigma ev).evar_source))) sigma in
-- 
cgit v1.2.3


From 2423629321d46c7facc59b4206bbb773725ec63d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 2 Jul 2020 15:55:20 +0200
Subject: Do not tamper with hints in Class_tactics.with_prods.

---
 tactics/class_tactics.ml | 59 +++++++++++++++++++++++++-----------------------
 1 file changed, 31 insertions(+), 28 deletions(-)

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index e28ce1b85a..5a8522359d 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -161,18 +161,26 @@ let e_give_exact flags h =
   Clenv.unify ~flags t1 <*> exact_no_check c
   end
 
-let unify_e_resolve flags (h, _) = Proofview.Goal.enter begin fun gls ->
-  let clenv', c = connect_hint_clenv h gls in
-  Clenv.res_pf ~with_evars:true ~with_classes:false ~flags clenv'
-  end
-
-let unify_resolve flags (h, _) = Proofview.Goal.enter begin fun gls ->
+let unify_resolve ~with_evars flags h diff = match diff with
+| None ->
+  Proofview.Goal.enter begin fun gls ->
   let clenv', _ = connect_hint_clenv h gls in
-  Clenv.res_pf ~with_evars:false ~with_classes:false ~flags clenv'
+  Clenv.res_pf ~with_evars ~with_classes:false ~flags clenv'
+  end
+| Some (diff, ty) ->
+  let () = assert (not h.hint_poly) in
+  Proofview.Goal.enter begin fun gl ->
+  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
+  Clenv.res_pf ~with_evars ~with_classes:false ~flags clenv
   end
 
 (** Application of a lemma using [refine] instead of the old [w_unify] *)
-let unify_resolve_refine flags (h, n) =
+let unify_resolve_refine flags h diff =
+  let len = match diff with None -> None | Some (diff, _) -> Some diff in
   Proofview.Goal.enter begin fun gls ->
   let { hint_term = c; hint_type = t; hint_uctx = ctx } = h in
   let open Clenv in
@@ -189,7 +197,7 @@ let unify_resolve_refine flags (h, n) =
           let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
           sigma, c, t
       in
-      let sigma', cl = Clenv.make_evar_clause env sigma ?len:n ty in
+      let sigma', cl = Clenv.make_evar_clause env sigma ?len ty in
       let term = applist (term, List.map (fun x -> x.hole_evar) cl.cl_holes) in
       let sigma' =
         Evarconv.(unify_leq_delay
@@ -198,9 +206,9 @@ let unify_resolve_refine flags (h, n) =
       in (sigma', term) end
   end
 
-let unify_resolve_refine flags clenv =
+let unify_resolve_refine flags h diff =
   Proofview.tclORELSE
-    (unify_resolve_refine flags clenv)
+    (unify_resolve_refine flags h diff)
     (fun (exn,info) ->
       match exn with
       | Evarconv.UnableToUnify _ ->
@@ -217,22 +225,17 @@ let with_prods nprods h f =
   if get_typeclasses_limit_intros () then
     Proofview.Goal.enter begin fun gl ->
       let { hint_term = c; hint_clnv = clenv; hint_poly = poly } = h in
-      if poly || Int.equal nprods 0 then
-        f (h, None)
+      if poly || Int.equal nprods 0 then f None
       else
         let sigma = Tacmach.New.project gl in
         let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma c in
         let diff = nb_prod sigma ty - nprods in
-        if (>=) diff 0 then
-          (* Was Some clenv... *)
-          let clenv = mk_clenv_from_n gl (Some diff) (c,ty) in
-          let h = { h with hint_clnv = clenv } in
-          f (h, Some diff)
+        if (>=) diff 0 then f (Some (diff, ty))
         else Tacticals.New.tclZEROMSG (str"Not enough premisses")
     end
   else Proofview.Goal.enter
          begin fun gl ->
-         if Int.equal nprods 0 then f (h, None)
+         if Int.equal nprods 0 then f None
          else Tacticals.New.tclZEROMSG (str"Not enough premisses") end
 
 let matches_pattern concl pat =
@@ -340,25 +343,25 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
            if get_typeclasses_filtered_unification () then
              let tac =
                with_prods nprods h
-                          (fun clenv ->
+                          (fun diff ->
                              matches_pattern concl p <*>
-                               unify_resolve_refine flags clenv)
+                               unify_resolve_refine flags h diff)
              in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
            else
              let tac =
-               with_prods nprods h (unify_resolve flags) in
+               with_prods nprods h (unify_resolve ~with_evars:false flags h) in
                Proofview.tclBIND (Proofview.with_shelf tac)
                   (fun (gls, ()) -> shelve_dependencies gls)
         | ERes_pf h ->
            if get_typeclasses_filtered_unification () then
              let tac = (with_prods nprods h
-                  (fun clenv ->
+                  (fun diff ->
                              matches_pattern concl p <*>
-                             unify_resolve_refine flags clenv)) in
+                             unify_resolve_refine flags h diff)) in
              Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
            else
              let tac =
-               with_prods nprods h (unify_e_resolve flags) in
+               with_prods nprods h (unify_resolve ~with_evars:true flags h) in
                Proofview.tclBIND (Proofview.with_shelf tac)
                   (fun (gls, ()) -> shelve_dependencies gls)
         | Give_exact h ->
@@ -366,12 +369,12 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
              let tac =
                matches_pattern concl p <*>
                  Proofview.Goal.enter
-                   (fun gl -> unify_resolve_refine flags (h, None)) in
+                   (fun gl -> unify_resolve_refine flags h None) in
              Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
            else
              e_give_exact flags h
       | Res_pf_THEN_trivial_fail h ->
-         let fst = with_prods nprods h (unify_e_resolve flags) in
+         let fst = with_prods nprods h (unify_resolve ~with_evars:true flags h) in
          let snd = if complete then Tacticals.New.tclIDTAC
                    else e_trivial_fail_db only_classes db_list local_db secvars in
          Tacticals.New.tclTHEN fst snd
@@ -1229,7 +1232,7 @@ let autoapply c i =
   let cty = Tacmach.New.pf_get_type_of gl c in
   let ce = mk_clenv_from gl (c,cty) in
   let h = { hint_term = c; hint_type = cty; hint_uctx = Univ.ContextSet.empty; hint_clnv = ce; hint_poly = false } in
-    unify_e_resolve flags (h, 0) <*>
+    unify_resolve ~with_evars:true flags h None <*>
       Proofview.tclEVARMAP >>= (fun sigma ->
       let sigma = Typeclasses.make_unresolvables
           (fun ev -> Typeclasses.all_goals ev (Lazy.from_val (snd (Evd.find sigma ev).evar_source))) sigma in
-- 
cgit v1.2.3


From 8db43cac35eaa8f2b8c4f8d777dfaafd1f02f27e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 2 Jul 2020 16:11:47 +0200
Subject: Do not do a round trip with auto hint representation in autoapply.

---
 tactics/class_tactics.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 5a8522359d..6c1bdca682 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1231,8 +1231,7 @@ let autoapply c i =
     (Hints.Hint_db.transparent_state hintdb) in
   let cty = Tacmach.New.pf_get_type_of gl c in
   let ce = mk_clenv_from gl (c,cty) in
-  let h = { hint_term = c; hint_type = cty; hint_uctx = Univ.ContextSet.empty; hint_clnv = ce; hint_poly = false } in
-    unify_resolve ~with_evars:true flags h None <*>
+  Clenv.res_pf ~with_evars:true ~with_classes:false ~flags ce <*>
       Proofview.tclEVARMAP >>= (fun sigma ->
       let sigma = Typeclasses.make_unresolvables
           (fun ev -> Typeclasses.all_goals ev (Lazy.from_val (snd (Evd.find sigma ev).evar_source))) sigma in
-- 
cgit v1.2.3


From b0aa5bd44d31e7b3dd93b22f1fdfdd7545421ec1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 2 Jul 2020 16:14:12 +0200
Subject: Move connect_hint_clenv from Auto to Hints.

---
 tactics/auto.ml   | 28 ----------------------------
 tactics/auto.mli  |  4 ----
 tactics/hints.ml  | 27 +++++++++++++++++++++++++++
 tactics/hints.mli |  3 +++
 4 files changed, 30 insertions(+), 32 deletions(-)

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 3287c1c354..f485e7f02e 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -12,7 +12,6 @@ open Pp
 open Util
 open Names
 open Termops
-open EConstr
 open Environ
 open Genredexpr
 open Tactics
@@ -69,33 +68,6 @@ let auto_unif_flags =
 
 (* Try unification with the precompiled clause, then use registered Apply *)
 
-let connect_hint_clenv h gl =
-  let { hint_term = c; hint_uctx = ctx; hint_clnv = clenv } = h in
-  (* [clenv] has been generated by a hint-making function, so the only relevant
-     data in its evarmap is the set of metas. The [evar_reset_evd] function
-     below just replaces the metas of sigma by those coming from the clenv. *)
-  let sigma = Tacmach.New.project gl in
-  let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in
-  (* Still, we need to update the universes *)
-  let clenv, c =
-    if h.hint_poly then
-      (* Refresh the instance of the hint *)
-      let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
-      let emap c = Vars.subst_univs_level_constr subst c in
-      let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
-      (* Only metas are mentioning the old universes. *)
-      let clenv = {
-        templval = Evd.map_fl emap clenv.templval;
-        templtyp = Evd.map_fl emap clenv.templtyp;
-        evd = Evd.map_metas emap evd;
-        env = Proofview.Goal.env gl;
-      } in
-      clenv, emap c
-    else
-      let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
-      { clenv with evd = evd ; env = Proofview.Goal.env gl }, c
-  in clenv, c
-
 let unify_resolve flags (h : hint) =
   Proofview.Goal.enter begin fun gl ->
   let clenv, c = connect_hint_clenv h gl in
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 903da143d2..bc2eee0e4c 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -12,7 +12,6 @@
 
 open Names
 open EConstr
-open Clenv
 open Pattern
 open Hints
 open Tactypes
@@ -23,9 +22,6 @@ val default_search_depth : int ref
 
 val auto_flags_of_state : TransparentState.t -> Unification.unify_flags
 
-val connect_hint_clenv
-  : hint -> Proofview.Goal.t -> clausenv * constr
-
 (** Try unification with the precompiled clause, then use registered Apply *)
 val unify_resolve : Unification.unify_flags -> hint -> unit Proofview.tactic
 
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 386224824f..9fac66515a 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1593,3 +1593,30 @@ struct
 
   let repr (h : t) = h.code.obj
 end
+
+let connect_hint_clenv h gl =
+  let { hint_term = c; hint_uctx = ctx; hint_clnv = clenv } = h in
+  (* [clenv] has been generated by a hint-making function, so the only relevant
+     data in its evarmap is the set of metas. The [evar_reset_evd] function
+     below just replaces the metas of sigma by those coming from the clenv. *)
+  let sigma = Tacmach.New.project gl in
+  let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in
+  (* Still, we need to update the universes *)
+  let clenv, c =
+    if h.hint_poly then
+      (* Refresh the instance of the hint *)
+      let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
+      let emap c = Vars.subst_univs_level_constr subst c in
+      let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
+      (* Only metas are mentioning the old universes. *)
+      let clenv = {
+        templval = Evd.map_fl emap clenv.templval;
+        templtyp = Evd.map_fl emap clenv.templtyp;
+        evd = Evd.map_metas emap evd;
+        env = Proofview.Goal.env gl;
+      } in
+      clenv, emap c
+    else
+      let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
+      { clenv with evd = evd ; env = Proofview.Goal.env gl }, c
+  in clenv, c
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 8243716624..1508b81d1f 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -239,6 +239,9 @@ val wrap_hint_warning_fun : env -> evar_map ->
   (evar_map -> 'a * evar_map) -> 'a * evar_map
 (** Variant of the above for non-tactics *)
 
+val connect_hint_clenv
+  : hint -> Proofview.Goal.t -> clausenv * constr
+
 (** Printing  hints *)
 
 val pr_searchtable : env -> evar_map -> Pp.t
-- 
cgit v1.2.3


From de16cf5411c2696044d5b17cccb3659d21a79921 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 2 Jul 2020 16:15:32 +0200
Subject: Make the Hint.hint type private.

---
 tactics/hints.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/hints.mli b/tactics/hints.mli
index 1508b81d1f..28db5b3618 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -39,7 +39,7 @@ type 'a hint_ast =
   | Unfold_nth of evaluable_global_reference       (* Hint Unfold *)
   | Extern     of Genarg.glob_generic_argument       (* Hint Extern *)
 
-type hint = {
+type hint = private {
   hint_term : constr;
   hint_type : types;
   hint_uctx : Univ.ContextSet.t;
-- 
cgit v1.2.3


From a666788182bce7059e6ba41b917b5ca6ab52ae13 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 16 Jul 2020 19:34:18 +0200
Subject: Code simplification around hint manipulation in Class_tactics.

We inline the clenv universe refreshing, since it was the only place in the
code that used it. Furthermore it was performing useless substitutions in
the clenv.
---
 proofs/clenv.ml          | 10 ----------
 proofs/clenv.mli         |  3 ---
 tactics/class_tactics.ml | 13 ++++++++++---
 3 files changed, 10 insertions(+), 16 deletions(-)

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 9bd7ccda5d..db76d08736 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -47,16 +47,6 @@ let clenv_meta_type clenv mv = Typing.meta_type clenv.env clenv.evd mv
 let clenv_value clenv = meta_instance clenv.env clenv.evd clenv.templval
 let clenv_type clenv = meta_instance clenv.env clenv.evd clenv.templtyp
 
-let refresh_undefined_univs clenv =
-  match EConstr.kind clenv.evd clenv.templval.rebus with
-  | Var _ -> clenv, Univ.empty_level_subst
-  | App (f, args) when isVar clenv.evd f -> clenv, Univ.empty_level_subst
-  | _ ->
-    let evd', subst = Evd.refresh_undefined_universes clenv.evd in
-    let map_freelisted f = { f with rebus = subst_univs_level_constr subst f.rebus } in
-      { clenv with evd = evd'; templval = map_freelisted clenv.templval;
-        templtyp = map_freelisted clenv.templtyp }, subst
-
 let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
 
 let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index fd1e2fe593..43e808dac7 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -45,9 +45,6 @@ val mk_clenv_from_n :
   Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv
 val mk_clenv_from_env : env -> evar_map -> int option -> EConstr.constr * EConstr.types -> clausenv
 
-(** Refresh the universes in a clenv *)
-val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst
-
 (** {6 linking of clenvs } *)
 
 val clenv_fchain :
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 6c1bdca682..279476badb 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -143,6 +143,12 @@ let auto_unif_flags ?(allowed_evars = AllowAll) st =
     resolve_evars = false
 }
 
+let refresh_undefined_univs clenv =
+  match EConstr.kind clenv.evd clenv.templval.rebus with
+  | Var _ -> clenv.evd, Univ.empty_level_subst
+  | App (f, args) when isVar clenv.evd f -> clenv.evd, Univ.empty_level_subst
+  | _ -> Evd.refresh_undefined_universes clenv.evd
+
 let e_give_exact flags h =
   let { hint_term = c; hint_clnv = clenv } = h in
   let open Tacmach.New in
@@ -150,8 +156,9 @@ let e_give_exact flags h =
   let sigma = project gl in
   let c, sigma =
     if h.hint_poly then
-      let clenv', subst = Clenv.refresh_undefined_univs clenv in
-      let evd = evars_reset_evd ~with_conv_pbs:true sigma clenv'.evd in
+      (* Should we really refresh all universes when we have the local ones at hand? *)
+      let evd, subst = refresh_undefined_univs clenv in
+      let evd = evars_reset_evd ~with_conv_pbs:true sigma evd in
       let c = Vars.subst_univs_level_constr subst c in
         c, evd
     else c, sigma
@@ -224,7 +231,7 @@ let unify_resolve_refine flags h diff =
 let with_prods nprods h f =
   if get_typeclasses_limit_intros () then
     Proofview.Goal.enter begin fun gl ->
-      let { hint_term = c; hint_clnv = clenv; hint_poly = poly } = h in
+      let { hint_term = c; hint_poly = poly } = h in
       if poly || Int.equal nprods 0 then f None
       else
         let sigma = Tacmach.New.project gl in
-- 
cgit v1.2.3


From e28edfdc3c373af7f5ca4fbd716c8c5753494d5a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 16 Jul 2020 20:06:07 +0200
Subject: Export a dedicated function that applies immediately a hint.

---
 tactics/auto.ml          | 6 +-----
 tactics/class_tactics.ml | 5 +----
 tactics/eauto.ml         | 5 +----
 tactics/hints.ml         | 6 ++++++
 tactics/hints.mli        | 3 +++
 5 files changed, 12 insertions(+), 13 deletions(-)

diff --git a/tactics/auto.ml b/tactics/auto.ml
index f485e7f02e..1ba35e9113 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -68,11 +68,7 @@ let auto_unif_flags =
 
 (* Try unification with the precompiled clause, then use registered Apply *)
 
-let unify_resolve flags (h : hint) =
-  Proofview.Goal.enter begin fun gl ->
-  let clenv, c = connect_hint_clenv h gl in
-  Clenv.res_pf ~flags clenv
-  end
+let unify_resolve flags h = Hints.hint_res_pf ~flags h
 
 let unify_resolve_nodelta h = unify_resolve auto_unif_flags h
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 279476badb..62470a60c0 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -170,10 +170,7 @@ let e_give_exact flags h =
 
 let unify_resolve ~with_evars flags h diff = match diff with
 | None ->
-  Proofview.Goal.enter begin fun gls ->
-  let clenv', _ = connect_hint_clenv h gls in
-  Clenv.res_pf ~with_evars ~with_classes:false ~flags clenv'
-  end
+  Hints.hint_res_pf ~with_evars ~with_classes:false ~flags h
 | Some (diff, ty) ->
   let () = assert (not h.hint_poly) in
   Proofview.Goal.enter begin fun gl ->
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 686303a2ab..1bdf36b56c 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -66,10 +66,7 @@ open Auto
 (***************************************************************************)
 
 let unify_e_resolve flags h =
-  Proofview.Goal.enter begin fun gl ->
-      let clenv', c = connect_hint_clenv h gl in
-      Clenv.res_pf ~with_evars:true ~with_classes:true ~flags clenv'
-    end
+  Hints.hint_res_pf ~with_evars:true ~with_classes:true ~flags h
 
 let hintmap_of sigma secvars concl =
   (* Warning: for computation sharing, we need to return a closure *)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 9fac66515a..683691d5c4 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1620,3 +1620,9 @@ let connect_hint_clenv h gl =
       let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
       { clenv with evd = evd ; env = Proofview.Goal.env gl }, c
   in clenv, c
+
+let hint_res_pf ?with_evars ?with_classes ?flags h =
+  Proofview.Goal.enter begin fun gl ->
+    let clenv, _ = connect_hint_clenv h gl in
+    Clenv.res_pf ?with_evars ?with_classes ?flags clenv
+  end
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 28db5b3618..d8b6458c27 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -242,6 +242,9 @@ val wrap_hint_warning_fun : env -> evar_map ->
 val connect_hint_clenv
   : hint -> Proofview.Goal.t -> clausenv * constr
 
+val hint_res_pf : ?with_evars:bool -> ?with_classes:bool ->
+  ?flags:Unification.unify_flags -> hint -> unit Proofview.tactic
+
 (** Printing  hints *)
 
 val pr_searchtable : env -> evar_map -> Pp.t
-- 
cgit v1.2.3


From 2e22662662ebb44a18b8950e3b2876d6787d2d2f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 16 Jul 2020 23:11:08 +0200
Subject: Tentatively more efficient implementation of e_give_exact for
 typeclasses.

The old code was refreshing the whole evarmap when only the constraints
introduced by the term would matter. Since exact hints never introduces
metas for missing binders, there is nothing to extract from the clenv,
so we can just generate a fresh universe substitution.
---
 tactics/class_tactics.ml | 15 ++++-----------
 1 file changed, 4 insertions(+), 11 deletions(-)

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 62470a60c0..64d62a89b0 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -143,24 +143,17 @@ let auto_unif_flags ?(allowed_evars = AllowAll) st =
     resolve_evars = false
 }
 
-let refresh_undefined_univs clenv =
-  match EConstr.kind clenv.evd clenv.templval.rebus with
-  | Var _ -> clenv.evd, Univ.empty_level_subst
-  | App (f, args) when isVar clenv.evd f -> clenv.evd, Univ.empty_level_subst
-  | _ -> Evd.refresh_undefined_universes clenv.evd
-
 let e_give_exact flags h =
-  let { hint_term = c; hint_clnv = clenv } = h in
+  let { hint_term = c; hint_uctx = ctx } = h in
   let open Tacmach.New in
   Proofview.Goal.enter begin fun gl ->
   let sigma = project gl in
   let c, sigma =
     if h.hint_poly then
-      (* Should we really refresh all universes when we have the local ones at hand? *)
-      let evd, subst = refresh_undefined_univs clenv in
-      let evd = evars_reset_evd ~with_conv_pbs:true sigma evd in
+      let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
+      let evd = Evd.merge_context_set Evd.univ_flexible sigma ctx in
       let c = Vars.subst_univs_level_constr subst c in
-        c, evd
+      c, evd
     else c, sigma
   in
   let (sigma, t1) = Typing.type_of (pf_env gl) sigma c in
-- 
cgit v1.2.3


From 70b7aabfdfecfc94fd5cbfd2fbf7b65cfaacdd63 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 17 Jul 2020 11:22:20 +0200
Subject: Remove dead code after the previous commit.

The costly universe refreshing functions were only used for typeclass hint
resolution, which now relies on the provided hint context.
---
 engine/evd.ml     |  5 -----
 engine/evd.mli    |  2 --
 engine/uState.ml  | 29 -----------------------------
 engine/uState.mli |  2 --
 4 files changed, 38 deletions(-)

diff --git a/engine/evd.ml b/engine/evd.ml
index c570f75c6b..e85cbc96b2 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -987,11 +987,6 @@ let check_constraints evd csts =
 let fix_undefined_variables evd =
   { evd with universes = UState.fix_undefined_variables evd.universes }
 
-let refresh_undefined_universes evd =
-  let uctx', subst = UState.refresh_undefined_univ_variables evd.universes in
-  let evd' = cmap (subst_univs_level_constr subst) {evd with universes = uctx'} in
-    evd', subst
-
 let nf_univ_variables evd =
   let subst, uctx' = UState.normalize_variables evd.universes in
   let evd' = {evd with universes = uctx'} in
diff --git a/engine/evd.mli b/engine/evd.mli
index 679173ca72..3f17e63034 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -643,8 +643,6 @@ val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst
 
 val fix_undefined_variables : evar_map -> evar_map
 
-val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_subst
-
 (** Universe minimization *)
 val minimize_universes : evar_map -> evar_map
 
diff --git a/engine/uState.ml b/engine/uState.ml
index d4cb59da26..ca0a21acf7 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -718,35 +718,6 @@ let fix_undefined_variables uctx =
   { uctx with univ_variables = vars';
     univ_algebraic = algs' }
 
-let refresh_undefined_univ_variables uctx =
-  let subst, ctx' = UnivGen.fresh_universe_context_set_instance uctx.local in
-  let subst_fn u = subst_univs_level_level subst u in
-  let alg = LSet.fold (fun u acc -> LSet.add (subst_fn u) acc)
-    uctx.univ_algebraic LSet.empty
-  in
-  let vars =
-    LMap.fold
-      (fun u v acc ->
-        LMap.add (subst_fn u)
-          (Option.map (subst_univs_level_universe subst) v) acc)
-      uctx.univ_variables LMap.empty
-  in
-  let weak = UPairSet.fold (fun (u,v) acc -> UPairSet.add (subst_fn u, subst_fn v) acc) uctx.weak_constraints UPairSet.empty in
-  let lbound = uctx.universes_lbound in
-  let declare g = LSet.fold (fun u g -> UGraph.add_universe u ~lbound ~strict:false g)
-      (ContextSet.levels ctx') g in
-  let initial = declare uctx.initial_universes in
-  let univs = declare UGraph.initial_universes in
-  let uctx' = {names = uctx.names;
-               local = ctx';
-               seff_univs = uctx.seff_univs;
-               univ_variables = vars; univ_algebraic = alg;
-               universes = univs;
-               universes_lbound = lbound;
-               initial_universes = initial;
-               weak_constraints = weak; } in
-    uctx', subst
-
 let minimize uctx =
   let open UnivMinim in
   let lbound = uctx.universes_lbound in
diff --git a/engine/uState.mli b/engine/uState.mli
index 45a0f9964e..607c6c9452 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -154,8 +154,6 @@ val abstract_undefined_variables : t -> t
 
 val fix_undefined_variables : t -> t
 
-val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst
-
 (** Universe minimization *)
 val minimize : t -> t
 
-- 
cgit v1.2.3


From 2a62e99b7fd73f58269527a1b646fae1b25570d5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 17 Jul 2020 12:01:51 +0200
Subject: Split the uses of connect_hint_clenv into two different functions.

The first one is encapsulating the clenv part, and is now purely internal,
while the other one provides an abstract interfact to get fresh term instances
from a hint.
---
 tactics/auto.ml          |  9 ++++-----
 tactics/class_tactics.ml | 40 +++++++++++++-------------------------
 tactics/eauto.ml         |  9 ++++-----
 tactics/hints.ml         | 50 +++++++++++++++++++++++++++++-------------------
 tactics/hints.mli        |  3 +--
 5 files changed, 52 insertions(+), 59 deletions(-)

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 1ba35e9113..0931c3e61e 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -15,7 +15,6 @@ open Termops
 open Environ
 open Genredexpr
 open Tactics
-open Clenv
 open Locus
 open Proofview.Notations
 open Hints
@@ -78,10 +77,10 @@ let unify_resolve_gen = function
 
 let exact h =
   Proofview.Goal.enter begin fun gl ->
-    let clenv', c = connect_hint_clenv h gl in
-    Tacticals.New.tclTHEN
-    (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
-    (exact_check c)
+    let env = Proofview.Goal.env gl in
+    let sigma = Proofview.Goal.sigma gl in
+    let sigma, c = Hints.fresh_hint env sigma h in
+    Proofview.Unsafe.tclEVARS sigma <*> exact_check c
   end
 
 (* Util *)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 64d62a89b0..c4ef32974c 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -144,18 +144,11 @@ let auto_unif_flags ?(allowed_evars = AllowAll) st =
 }
 
 let e_give_exact flags h =
-  let { hint_term = c; hint_uctx = ctx } = h in
   let open Tacmach.New in
   Proofview.Goal.enter begin fun gl ->
+  let env = Proofview.Goal.env gl in
   let sigma = project gl in
-  let c, sigma =
-    if h.hint_poly then
-      let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
-      let evd = Evd.merge_context_set Evd.univ_flexible sigma ctx in
-      let c = Vars.subst_univs_level_constr subst c in
-      c, evd
-    else c, sigma
-  in
+  let sigma, c = Hints.fresh_hint env sigma h in
   let (sigma, t1) = Typing.type_of (pf_env gl) sigma c in
   Proofview.Unsafe.tclEVARS sigma <*>
   Clenv.unify ~flags t1 <*> exact_no_check c
@@ -179,28 +172,21 @@ let unify_resolve ~with_evars flags h diff = match diff with
 let unify_resolve_refine flags h diff =
   let len = match diff with None -> None | Some (diff, _) -> Some diff in
   Proofview.Goal.enter begin fun gls ->
-  let { hint_term = c; hint_type = t; hint_uctx = ctx } = h in
   let open Clenv in
   let env = Proofview.Goal.env gls in
   let concl = Proofview.Goal.concl gls in
   Refine.refine ~typecheck:false begin fun sigma ->
-      let sigma, term, ty =
-        if h.hint_poly then
-          let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
-          let map c = Vars.subst_univs_level_constr subst c in
-          let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
-          sigma, map c, map t
-        else
-          let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
-          sigma, c, t
-      in
-      let sigma', cl = Clenv.make_evar_clause env sigma ?len ty in
-      let term = applist (term, List.map (fun x -> x.hole_evar) cl.cl_holes) in
-      let sigma' =
-        Evarconv.(unify_leq_delay
-                    ~flags:(default_flags_of flags.core_unify_flags.modulo_delta)
-                              env sigma' cl.cl_concl concl)
-      in (sigma', term) end
+    let sigma, term = Hints.fresh_hint env sigma h in
+    let ty = Retyping.get_type_of env sigma term in
+    let sigma, cl = Clenv.make_evar_clause env sigma ?len ty in
+    let term = applist (term, List.map (fun x -> x.hole_evar) cl.cl_holes) in
+    let sigma =
+      Evarconv.(unify_leq_delay
+                  ~flags:(default_flags_of flags.core_unify_flags.modulo_delta)
+                            env sigma cl.cl_concl concl)
+    in
+    (sigma, term)
+    end
   end
 
 let unify_resolve_refine flags h diff =
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 1bdf36b56c..9a554b117e 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -19,7 +19,6 @@ open Tacticals
 open Tacmach
 open Evd
 open Tactics
-open Clenv
 open Auto
 open Genredexpr
 open Tactypes
@@ -84,10 +83,10 @@ let hintmap_of sigma secvars concl =
 
 let e_exact flags h =
   Proofview.Goal.enter begin fun gl ->
-    let clenv', c = connect_hint_clenv h gl in
-    Tacticals.New.tclTHEN
-    (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
-    (e_give_exact c)
+    let env = Proofview.Goal.env gl in
+    let sigma = Proofview.Goal.sigma gl in
+    let sigma, c = Hints.fresh_hint env sigma h in
+    Proofview.Unsafe.tclEVARS sigma <*> e_give_exact c
   end
 
 let rec e_trivial_fail_db db_list local_db =
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 683691d5c4..e029e4628d 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1595,34 +1595,44 @@ struct
 end
 
 let connect_hint_clenv h gl =
-  let { hint_term = c; hint_uctx = ctx; hint_clnv = clenv } = h in
+  let { hint_uctx = ctx; hint_clnv = clenv } = h in
   (* [clenv] has been generated by a hint-making function, so the only relevant
      data in its evarmap is the set of metas. The [evar_reset_evd] function
      below just replaces the metas of sigma by those coming from the clenv. *)
   let sigma = Tacmach.New.project gl in
   let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in
   (* Still, we need to update the universes *)
-  let clenv, c =
-    if h.hint_poly then
-      (* Refresh the instance of the hint *)
-      let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
-      let emap c = Vars.subst_univs_level_constr subst c in
-      let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
-      (* Only metas are mentioning the old universes. *)
-      let clenv = {
-        templval = Evd.map_fl emap clenv.templval;
-        templtyp = Evd.map_fl emap clenv.templtyp;
-        evd = Evd.map_metas emap evd;
-        env = Proofview.Goal.env gl;
-      } in
-      clenv, emap c
-    else
-      let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
-      { clenv with evd = evd ; env = Proofview.Goal.env gl }, c
-  in clenv, c
+  if h.hint_poly then
+    (* Refresh the instance of the hint *)
+    let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
+    let emap c = Vars.subst_univs_level_constr subst c in
+    let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
+    (* Only metas are mentioning the old universes. *)
+    let clenv = {
+      templval = Evd.map_fl emap clenv.templval;
+      templtyp = Evd.map_fl emap clenv.templtyp;
+      evd = Evd.map_metas emap evd;
+      env = Proofview.Goal.env gl;
+    } in
+    clenv
+  else
+    let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
+    { clenv with evd = evd ; env = Proofview.Goal.env gl }
+
+let fresh_hint env sigma h =
+  let { hint_term = c; hint_uctx = ctx } = h in
+  if h.hint_poly then
+    (* Refresh the instance of the hint *)
+    let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
+    let c = Vars.subst_univs_level_constr subst c in
+    let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
+    sigma, c
+  else
+    let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
+    sigma, c
 
 let hint_res_pf ?with_evars ?with_classes ?flags h =
   Proofview.Goal.enter begin fun gl ->
-    let clenv, _ = connect_hint_clenv h gl in
+    let clenv = connect_hint_clenv h gl in
     Clenv.res_pf ?with_evars ?with_classes ?flags clenv
   end
diff --git a/tactics/hints.mli b/tactics/hints.mli
index d8b6458c27..f0fed75828 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -239,8 +239,7 @@ val wrap_hint_warning_fun : env -> evar_map ->
   (evar_map -> 'a * evar_map) -> 'a * evar_map
 (** Variant of the above for non-tactics *)
 
-val connect_hint_clenv
-  : hint -> Proofview.Goal.t -> clausenv * constr
+val fresh_hint : env -> evar_map -> hint -> evar_map * constr
 
 val hint_res_pf : ?with_evars:bool -> ?with_classes:bool ->
   ?flags:Unification.unify_flags -> hint -> unit Proofview.tactic
-- 
cgit v1.2.3


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


From 52894e97f045c257ba5f4a7c9d64c48fa1913994 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 12 Aug 2020 14:14:37 +0200
Subject: Cosmetic changes as suggested by SkySkimmer.

---
 tactics/class_tactics.ml | 7 ++-----
 tactics/hints.ml         | 5 ++---
 2 files changed, 4 insertions(+), 8 deletions(-)

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 1fadc164bf..36544883aa 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -179,11 +179,8 @@ let unify_resolve_refine flags h diff =
     let ty = Retyping.get_type_of env sigma term in
     let sigma, cl = Clenv.make_evar_clause env sigma ?len ty in
     let term = applist (term, List.map (fun x -> x.hole_evar) cl.cl_holes) in
-    let sigma =
-      Evarconv.(unify_leq_delay
-                  ~flags:(default_flags_of flags.core_unify_flags.modulo_delta)
-                            env sigma cl.cl_concl concl)
-    in
+    let flags = Evarconv.default_flags_of flags.core_unify_flags.modulo_delta in
+    let sigma = Evarconv.unify_leq_delay ~flags env sigma cl.cl_concl concl in
     (sigma, term)
     end
   end
diff --git a/tactics/hints.ml b/tactics/hints.ml
index e029e4628d..7b203c3d51 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1608,13 +1608,12 @@ let connect_hint_clenv h gl =
     let emap c = Vars.subst_univs_level_constr subst c in
     let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
     (* Only metas are mentioning the old universes. *)
-    let clenv = {
+    {
       templval = Evd.map_fl emap clenv.templval;
       templtyp = Evd.map_fl emap clenv.templtyp;
       evd = Evd.map_metas emap evd;
       env = Proofview.Goal.env gl;
-    } in
-    clenv
+    }
   else
     let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
     { clenv with evd = evd ; env = Proofview.Goal.env gl }
-- 
cgit v1.2.3


From 404314c00175fcd67468bc0875c697d1c88d4650 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 24 Jul 2020 11:46:13 +0200
Subject: Add overlays.

---
 dev/ci/user-overlays/12720-ppedrot-factor-class-hint-clenv.sh | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 dev/ci/user-overlays/12720-ppedrot-factor-class-hint-clenv.sh

diff --git a/dev/ci/user-overlays/12720-ppedrot-factor-class-hint-clenv.sh b/dev/ci/user-overlays/12720-ppedrot-factor-class-hint-clenv.sh
new file mode 100644
index 0000000000..e57f95ef19
--- /dev/null
+++ b/dev/ci/user-overlays/12720-ppedrot-factor-class-hint-clenv.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "12720" ] || [ "$CI_BRANCH" = "factor-class-hint-clenv" ]; then
+
+    coqhammer_CI_REF=factor-class-hint-clenv
+    coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer
+
+fi
-- 
cgit v1.2.3