Merge PR #12505: Cleanup the Hints API

Reviewed-by: herbelin

1 files changed, 21 insertions, 19 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 681c4e910f..f041af1db1 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -29,7 +29,7 @@ open Hints
 (*          tactics with a trace mechanism for automatic search           *)
 (**************************************************************************)
 
-let priority l = List.filter (fun (_, hint) -> Int.equal hint.pri 0) l
+let priority l = List.filter (fun (_, hint) -> Int.equal (FullHint.priority hint) 0) l
 
 let compute_secvars gl =
   let hyps = Proofview.Goal.hyps gl in
@@ -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 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. *)
@@ -77,7 +78,7 @@ let connect_hint_clenv ~poly (c, _, ctx) clenv gl =
   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 poly then
+    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
@@ -95,22 +96,22 @@ 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 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 h gl in
   let clenv = clenv_unique_resolver ~flags clenv gl in
   Clenvtac.clenv_refine clenv
   end
 
-let unify_resolve_nodelta poly h = unify_resolve ~poly auto_unif_flags h
+let unify_resolve_nodelta h = unify_resolve auto_unif_flags h
 
-let unify_resolve_gen ~poly = function
-  | None -> unify_resolve_nodelta poly
-  | Some flags -> unify_resolve ~poly flags
+let unify_resolve_gen = function
+  | None -> unify_resolve_nodelta
+  | Some flags -> unify_resolve flags
 
-let exact poly (c,clenv) =
+let exact h =
   Proofview.Goal.enter begin fun gl ->
-    let clenv', c = connect_hint_clenv ~poly c clenv gl in
+    let clenv', c = connect_hint_clenv h gl in
     Tacticals.New.tclTHEN
     (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
     (exact_check c)
@@ -381,16 +382,16 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl =
           in List.map (fun x -> (Some flags,x)) l)
         (local_db::db_list)
 
-and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=dbname})) =
+and tac_of_hint dbg db_list local_db concl (flags, h) =
   let tactic = function
-    | Res_pf (c,cl) -> unify_resolve_gen ~poly flags (c,cl)
+    | Res_pf h -> unify_resolve_gen 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 h
+    | Res_pf_THEN_trivial_fail h ->
       Tacticals.New.tclTHEN
-        (unify_resolve_gen ~poly flags (c,cl))
+        (unify_resolve_gen 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)
@@ -403,16 +404,17 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=
          Tacticals.New.tclFAIL ~info 0 (str"Unbound reference")
        end
     | Extern tacast ->
+      let p = FullHint.pattern h in
       conclPattern concl p tacast
   in
   let pr_hint env sigma =
-    let origin = match dbname with
+    let origin = match FullHint.database h with
     | None -> mt ()
     | Some n -> str " (in " ++ str n ++ str ")"
     in
-    pr_hint env sigma t ++ origin
+    FullHint.print env sigma h ++ origin
   in
-  tclLOG dbg pr_hint (run_hint t tactic)
+  tclLOG dbg pr_hint (FullHint.run h tactic)
 
 and trivial_resolve sigma dbg mod_delta db_list local_db secvars cl =
   try