Merge PR #12720: Factor code related to class hint clenv

Reviewed-by: SkySkimmer
Reviewed-by: herbelin

6 files changed, 105 insertions, 125 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 3287c1c354..0931c3e61e 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -12,11 +12,9 @@ open Pp
 open Util
 open Names
 open Termops
-open EConstr
 open Environ
 open Genredexpr
 open Tactics
-open Clenv
 open Locus
 open Proofview.Notations
 open Hints
@@ -69,38 +67,7 @@ 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
-  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
 
@@ -110,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/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/class_tactics.ml b/tactics/class_tactics.ml
index 63cafbf76d..36544883aa 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -144,61 +144,50 @@ let auto_unif_flags ?(allowed_evars = AllowAll) st =
 }
 
 let e_give_exact flags h =
-  let { hint_term = c; hint_clnv = clenv } = 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 clenv', subst = Clenv.refresh_undefined_univs clenv in
-      let evd = evars_reset_evd ~with_conv_pbs:true sigma clenv'.evd 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
   end
 
-let unify_e_resolve flags = begin fun gls (h, _) ->
-  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 clenv', _ = connect_hint_clenv h gls in
-  Clenv.res_pf ~with_evars:false ~with_classes:false ~flags clenv'
+let unify_resolve ~with_evars flags h diff = match diff with
+| None ->
+  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 ->
+  let env = Proofview.Goal.env gl in
+  let sigma = Tacmach.New.project 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
 
 (** 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 diff =
+  let len = match diff with None -> None | Some (diff, _) -> Some diff in
+  Proofview.Goal.enter begin fun gls ->
   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:n 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 unify_resolve_refine flags gl clenv =
+    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 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
+
+let unify_resolve_refine flags h diff =
   Proofview.tclORELSE
-    (unify_resolve_refine flags gl clenv)
+    (unify_resolve_refine flags h diff)
     (fun (exn,info) ->
       match exn with
       | Evarconv.UnableToUnify _ ->
@@ -211,35 +200,21 @@ 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_poly = poly } = h in
+      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 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 gl (h, None)
+         if Int.equal nprods 0 then f None
          else Tacticals.New.tclZEROMSG (str"Not enough premisses") end
 
 let matches_pattern concl pat =
@@ -347,25 +322,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 gl clenv ->
+                          (fun diff ->
                              matches_pattern concl p <*>
-                               unify_resolve_refine flags gl 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 gl clenv ->
+                  (fun diff ->
                              matches_pattern concl p <*>
-                             unify_resolve_refine flags gl 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 ->
@@ -373,12 +348,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 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
       | 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
@@ -1235,8 +1210,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_e_resolve flags gl (h, 0) <*>
+  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
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 686303a2ab..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
@@ -66,10 +65,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 *)
@@ -87,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 58bebe319b..41b200bb83 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1599,3 +1599,45 @@ struct
 
   let repr (h : t) = h.code.obj
 end
+
+let connect_hint_clenv h gl =
+  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 *)
+  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. *)
+    {
+      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;
+    }
+  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
+    Clenv.res_pf ?with_evars ?with_classes ?flags clenv
+  end
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 8243716624..f0fed75828 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;
@@ -239,6 +239,11 @@ val wrap_hint_warning_fun : env -> evar_map ->
   (evar_map -> 'a * evar_map) -> 'a * evar_map
 (** Variant of the above for non-tactics *)
 
+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
+
 (** Printing  hints *)
 
 val pr_searchtable : env -> evar_map -> Pp.t