Wrap the content of full hints into a record.

1 files changed, 10 insertions, 9 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index a73db95884..4ed01d4e65 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -69,7 +69,8 @@ let auto_unif_flags =
 
 (* Try unification with the precompiled clause, then use registered Apply *)
 
-let connect_hint_clenv ~poly (c, _, ctx) clenv gl =
+let connect_hint_clenv ~poly 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. *)
@@ -95,9 +96,9 @@ let connect_hint_clenv ~poly (c, _, ctx) clenv gl =
       { clenv with evd = evd ; env = Proofview.Goal.env gl }, c
   in clenv, c
 
-let unify_resolve ~poly flags ((c : raw_hint), clenv) =
+let unify_resolve ~poly flags (h : hint) =
   Proofview.Goal.enter begin fun gl ->
-  let clenv, c = connect_hint_clenv ~poly c clenv gl in
+  let clenv, c = connect_hint_clenv ~poly h gl in
   let clenv = clenv_unique_resolver ~flags clenv gl in
   Clenvtac.clenv_refine clenv
   end
@@ -108,9 +109,9 @@ let unify_resolve_gen ~poly = function
   | None -> unify_resolve_nodelta poly
   | Some flags -> unify_resolve ~poly flags
 
-let exact poly (c,clenv) =
+let exact poly h =
   Proofview.Goal.enter begin fun gl ->
-    let clenv', c = connect_hint_clenv ~poly c clenv gl in
+    let clenv', c = connect_hint_clenv ~poly h gl in
     Tacticals.New.tclTHEN
     (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
     (exact_check c)
@@ -384,14 +385,14 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl =
 and tac_of_hint dbg db_list local_db concl (flags, h) =
   let poly = FullHint.is_polymorphic h in
   let tactic = function
-    | Res_pf (c,cl) -> unify_resolve_gen ~poly flags (c,cl)
+    | Res_pf h -> unify_resolve_gen ~poly flags h
     | ERes_pf _ -> Proofview.Goal.enter (fun gl ->
         let info = Exninfo.reify () in
         Tacticals.New.tclZEROMSG ~info (str "eres_pf"))
-    | Give_exact (c, cl)  -> exact poly (c, cl)
-    | Res_pf_THEN_trivial_fail (c,cl) ->
+    | Give_exact h  -> exact poly h
+    | Res_pf_THEN_trivial_fail h ->
       Tacticals.New.tclTHEN
-        (unify_resolve_gen ~poly flags (c,cl))
+        (unify_resolve_gen ~poly flags h)
         (* With "(debug) trivial", we shouldn't end here, and
            with "debug auto" we don't display the details of inner trivial *)
         (trivial_fail_db (no_dbg dbg) (not (Option.is_empty flags)) db_list local_db)