Export a dedicated function that applies immediately a hint.

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