Merge PR #12505: Cleanup the Hints API

Reviewed-by: herbelin

8 files changed, 189 insertions, 175 deletions

diff --git a/dev/ci/user-overlays/12505-ppedrot-factor-hint-flags.sh b/dev/ci/user-overlays/12505-ppedrot-factor-hint-flags.sh
new file mode 100644
index 0000000000..ced0d95945
--- /dev/null
+++ b/dev/ci/user-overlays/12505-ppedrot-factor-hint-flags.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "12505" ] || [ "$CI_BRANCH" = "factor-hint-flags" ]; then
+
+    fiat_parsers_CI_REF="factor-hint-flags"
+    fiat_parsers_CI_GITURL=https://github.com/ppedrot/fiat
+
+fi
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 3dd5059e5d..db3631daa4 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -205,10 +205,10 @@ open Hints
 
 let extend_with_auto_hints env sigma l seq =
   let f (seq,sigma) p_a_t =
-    match repr_hint p_a_t.code with
-    | Res_pf (c,_) | Give_exact (c,_)
-    | Res_pf_THEN_trivial_fail (c,_) ->
-      let (c, _, _) = c in
+    match FullHint.repr p_a_t with
+    | Res_pf c | Give_exact c
+    | Res_pf_THEN_trivial_fail c ->
+      let c = c.hint_term in
       (match  EConstr.destRef sigma c with
        | exception Constr.DestKO -> seq, sigma
        | gr, _ ->
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
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 33deefd0bd..903da143d2 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -24,10 +24,10 @@ val default_search_depth : int ref
 val auto_flags_of_state : TransparentState.t -> Unification.unify_flags
 
 val connect_hint_clenv
-  : poly:bool -> raw_hint -> clausenv -> Proofview.Goal.t -> clausenv * constr
+  : hint -> Proofview.Goal.t -> clausenv * constr
 
 (** Try unification with the precompiled clause, then use registered Apply *)
-val unify_resolve : poly:bool -> Unification.unify_flags -> (raw_hint * clausenv) -> unit Proofview.tactic
+val unify_resolve : Unification.unify_flags -> hint -> unit Proofview.tactic
 
 (** [ConclPattern concl pat tacast]:
    if the term concl matches the pattern pat, (in sense of
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 195073d7aa..484aab2f00 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -144,13 +144,13 @@ let auto_unif_flags ?(allowed_evars = AllowAll) st =
     resolve_evars = false
 }
 
-let e_give_exact flags poly (c,clenv) =
+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 sigma = project gl in
-  let (c, _, _) = c in
   let c, sigma =
-    if poly then
+    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
@@ -173,23 +173,24 @@ let clenv_unique_resolver_tac with_evars ~flags clenv' =
        Clenvtac.clenv_refine ~with_evars ~with_classes:false clenv'
   end
 
-let unify_e_resolve poly flags = begin fun gls (c,_,clenv) ->
-  let clenv', c = connect_hint_clenv ~poly c clenv gls in
+let unify_e_resolve flags = begin fun gls (h, _) ->
+  let clenv', c = connect_hint_clenv h gls in
   clenv_unique_resolver_tac true ~flags clenv' end
 
-let unify_resolve poly flags = begin fun gls (c,_,clenv) ->
-  let clenv', _ = connect_hint_clenv ~poly c clenv gls in
+let unify_resolve flags = begin fun gls (h, _) ->
+  let clenv', _ = connect_hint_clenv h gls in
   clenv_unique_resolver_tac false ~flags clenv'
   end
 
 (** Application of a lemma using [refine] instead of the old [w_unify] *)
-let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) =
+let unify_resolve_refine flags gls (h, n) =
+  let { hint_term = c; hint_type = t; hint_uctx = ctx; hint_clnv = clenv } = 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 poly then
+        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
@@ -206,9 +207,9 @@ let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) =
                               env sigma' cl.cl_concl concl)
       in (sigma', term) end
 
-let unify_resolve_refine poly flags gl clenv =
+let unify_resolve_refine flags gl clenv =
   Proofview.tclORELSE
-    (unify_resolve_refine poly flags gl clenv)
+    (unify_resolve_refine flags gl clenv)
     (fun (exn,info) ->
       match exn with
       | Evarconv.UnableToUnify _ ->
@@ -221,8 +222,8 @@ let unify_resolve_refine poly flags gl clenv =
 (** Dealing with goals of the form A -> B and hints of the form
   C -> A -> B.
 *)
-let clenv_of_prods poly nprods (c, clenv) gl =
-  let (c, _, _) = c in
+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
@@ -234,20 +235,22 @@ let clenv_of_prods poly nprods (c, clenv) gl =
             mk_clenv_from_n gl (Some diff) (c,ty))
     else None
 
-let with_prods nprods poly (c, clenv) f =
+let with_prods nprods h f =
   if get_typeclasses_limit_intros () then
     Proofview.Goal.enter begin fun gl ->
-      try match clenv_of_prods poly nprods (c, clenv) gl with
+      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') -> f gl (c, diff, clenv')
+          | 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
         Tacticals.New.tclZEROMSG ~info (CErrors.print e) end
   else Proofview.Goal.enter
          begin fun gl ->
-         if Int.equal nprods 0 then f gl (c, None, clenv)
+         if Int.equal nprods 0 then f gl (h, None)
          else Tacticals.New.tclZEROMSG (str"Not enough premisses") end
 
 let matches_pattern concl pat =
@@ -346,44 +349,47 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
     with e when CErrors.noncritical e -> AllowAll
   in
   let tac_of_hint =
-    fun (flags, {pri = b; pat = p; poly = poly; code = t; secvars; name = name}) ->
+    fun (flags, h) ->
+      let b = FullHint.priority h in
+      let p = FullHint.pattern h in
+      let name = FullHint.name h in
       let tac = function
-        | Res_pf (term,cl) ->
+        | Res_pf h ->
            if get_typeclasses_filtered_unification () then
              let tac =
-               with_prods nprods poly (term,cl)
+               with_prods nprods h
                           (fun gl clenv ->
                              matches_pattern concl p <*>
-                               unify_resolve_refine poly flags gl clenv)
+                               unify_resolve_refine flags gl clenv)
              in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
            else
              let tac =
-               with_prods nprods poly (term,cl) (unify_resolve poly flags) in
+               with_prods nprods h (unify_resolve flags) in
                Proofview.tclBIND (Proofview.with_shelf tac)
                   (fun (gls, ()) -> shelve_dependencies gls)
-        | ERes_pf (term,cl) ->
+        | ERes_pf h ->
            if get_typeclasses_filtered_unification () then
-             let tac = (with_prods nprods poly (term,cl)
+             let tac = (with_prods nprods h
                   (fun gl clenv ->
                              matches_pattern concl p <*>
-                             unify_resolve_refine poly flags gl clenv)) in
+                             unify_resolve_refine flags gl clenv)) in
              Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
            else
              let tac =
-               with_prods nprods poly (term,cl) (unify_e_resolve poly flags) in
+               with_prods nprods h (unify_e_resolve flags) in
                Proofview.tclBIND (Proofview.with_shelf tac)
                   (fun (gls, ()) -> shelve_dependencies gls)
-        | Give_exact (c,clenv) ->
+        | Give_exact h ->
            if get_typeclasses_filtered_unification () then
              let tac =
                matches_pattern concl p <*>
                  Proofview.Goal.enter
-                   (fun gl -> unify_resolve_refine poly flags gl (c,None,clenv)) in
+                   (fun gl -> unify_resolve_refine flags gl (h, None)) in
              Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
            else
-             e_give_exact flags poly (c,clenv)
-      | Res_pf_THEN_trivial_fail (term,cl) ->
-         let fst = with_prods nprods poly (term,cl) (unify_e_resolve poly flags) in
+             e_give_exact flags h
+      | Res_pf_THEN_trivial_fail h ->
+         let fst = with_prods nprods h (unify_e_resolve flags) 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
@@ -391,7 +397,7 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
          Proofview.tclPROGRESS (unfold_in_concl [AllOccurrences,c])
       | Extern tacast -> conclPattern concl p tacast
       in
-      let tac = run_hint t tac in
+      let tac = FullHint.run h tac in
       let tac = if complete then Tacticals.New.tclCOMPLETE tac else tac in
       let pp =
         match p with
@@ -399,9 +405,9 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
            str " with pattern " ++ Printer.pr_constr_pattern_env env sigma pat
         | _ -> mt ()
       in
-        match repr_hint t with
-        | Extern _ -> (tac, b, true, name, lazy (pr_hint env sigma t ++ pp))
-        | _ -> (tac, b, false, name, lazy (pr_hint env sigma t ++ pp))
+        match FullHint.repr h with
+        | Extern _ -> (tac, b, true, name, lazy (FullHint.print env sigma h ++ pp))
+        | _ -> (tac, b, false, name, lazy (FullHint.print env sigma h ++ pp))
   in
   let hint_of_db = hintmap_of sigma hdc secvars concl in
   let hintl = List.map_filter (fun db -> match hint_of_db db with
@@ -499,7 +505,7 @@ let evars_to_goals p evm =
   else Some (goals, nongoals)
 
 (** Making local hints  *)
-let make_resolve_hyp env sigma st flags only_classes pri decl =
+let make_resolve_hyp env sigma st only_classes pri decl =
   let id = NamedDecl.get_id decl in
   let cty = Evarutil.nf_evar sigma (NamedDecl.get_type decl) in
   let rec iscl env ty =
@@ -524,13 +530,11 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
             (List.map_append
              (fun (path,info,c) ->
               let h = IsConstr (EConstr.of_constr c,Univ.ContextSet.empty) [@ocaml.warning "-3"] in
-              make_resolves env sigma ~name:(PathHints path)
-                  (true,false,not !Flags.quiet) info ~check:true ~poly:false
-                 h)
+              make_resolves env sigma ~name:(PathHints path) info ~check:true ~poly:false h)
                hints)
         else []
       in
-        (hints @ make_resolves env sigma flags pri ~name ~check:false ~poly:false (IsGlobRef id))
+        (hints @ make_resolves env sigma pri ~name ~check:false ~poly:false (IsGlobRef id))
     else []
 
 let make_hints g (modes,st) only_classes sign =
@@ -546,7 +550,7 @@ let make_hints g (modes,st) only_classes sign =
         in
         if consider then
           let hint =
-            pf_apply make_resolve_hyp g st (true,false,false) only_classes empty_hint_info hyp
+            pf_apply make_resolve_hyp g st only_classes empty_hint_info hyp
           in hint @ hints
         else hints)
       ([]) sign
@@ -793,7 +797,7 @@ module Search = struct
     let decl = Tacmach.New.pf_last_hyp gl in
     let hint =
       make_resolve_hyp env sigma (Hint_db.transparent_state info.search_hints)
-                       (true,false,false) info.search_only_classes empty_hint_info decl in
+                       info.search_only_classes empty_hint_info decl in
     let ldb = Hint_db.add_list env sigma hint info.search_hints in
     let info' =
       { info with search_hints = ldb; last_tac = lazy (str"intro");
@@ -1246,7 +1250,8 @@ 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
-    unify_e_resolve false flags gl ((c,cty,Univ.ContextSet.empty),0,ce) <*>
+  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) <*>
       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 c2eabffd44..0ff90bc046 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -65,9 +65,9 @@ open Auto
 (* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *)
 (***************************************************************************)
 
-let unify_e_resolve poly flags (c,clenv) =
+let unify_e_resolve flags 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
       let clenv' = clenv_unique_resolver ~flags clenv' gl in
       Proofview.tclTHEN
         (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
@@ -88,9 +88,9 @@ let hintmap_of sigma secvars concl =
      else (fun db -> Hint_db.map_auto sigma ~secvars hdc concl db)
    (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)
 
-let e_exact poly flags (c,clenv) =
+let e_exact flags 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))
     (e_give_exact c)
@@ -120,23 +120,23 @@ and e_my_find_search env sigma db_list local_db secvars concl =
           List.map (fun x -> flags, x) (hint_of_db db)) (local_db::db_list)
   in
   let tac_of_hint =
-    fun (st, {pri = b; pat = p; code = t; poly = poly}) ->
-      let b = match Hints.repr_hint t with
+    fun (st, h) ->
+      let b = match FullHint.repr h with
       | Unfold_nth _ -> 1
-      | _ -> b
+      | _ -> FullHint.priority h
       in
       let tac = function
-      | Res_pf (term,cl) -> unify_resolve ~poly st (term,cl)
-      | ERes_pf (term,cl) -> unify_e_resolve poly st (term,cl)
-      | Give_exact (c,cl) -> e_exact poly st (c,cl)
-      | Res_pf_THEN_trivial_fail (term,cl) ->
-        Tacticals.New.tclTHEN (unify_e_resolve poly st (term,cl))
+      | Res_pf h -> unify_resolve st h
+      | ERes_pf h -> unify_e_resolve st h
+      | Give_exact h -> e_exact st h
+      | Res_pf_THEN_trivial_fail h ->
+        Tacticals.New.tclTHEN (unify_e_resolve st h)
           (e_trivial_fail_db db_list local_db)
       | Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl
-      | Extern tacast -> conclPattern concl p tacast
+      | Extern tacast -> conclPattern concl (FullHint.pattern h) tacast
       in
-      let tac = run_hint t tac in
-      (tac, b, lazy (pr_hint env sigma t))
+      let tac = FullHint.run h tac in
+      (tac, b, lazy (FullHint.print env sigma h))
   in
   List.map tac_of_hint hintl
 
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 0c23532e12..7a5615dd8e 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -135,15 +135,20 @@ type 'a with_uid = {
   uid : KerName.t;
 }
 
-type raw_hint = constr * types * Univ.ContextSet.t
-
-type hint = (raw_hint * clausenv) hint_ast with_uid
+type raw_hint = constr * types * Univ.ContextSet.t * bool (* poly *)
+
+type hint = {
+  hint_term : constr;
+  hint_type : types;
+  hint_uctx : Univ.ContextSet.t;
+  hint_clnv : clausenv;
+  hint_poly : bool;
+  (** Is the hint polymorpic and hence should be refreshed at each application *)
+}
 
 type 'a with_metadata =
   { pri     : int
   (** A number lower is higher priority *)
-  ; poly    : bool
-  (** Is the hint polymorpic and hence should be refreshed at each application *)
   ; pat     : constr_pattern option
   (** A pattern for the concl of the Goal *)
   ; name    : hints_path_atom
@@ -156,7 +161,7 @@ type 'a with_metadata =
   (** the tactic to apply when the concl matches pat *)
   }
 
-type full_hint = hint with_metadata
+type full_hint = hint hint_ast with_uid with_metadata
 
 type hint_entry = GlobRef.t option *
   raw_hint hint_ast with_uid with_metadata
@@ -300,19 +305,21 @@ let strip_params env sigma c =
   | _ -> c
 
 let instantiate_hint env sigma p =
-  let mk_clenv (c, cty, ctx) =
+  let mk_clenv (c, cty, ctx, poly) =
     let sigma = Evd.merge_context_set univ_flexible sigma ctx in
     let cl = mk_clenv_from_env env sigma None (c,cty) in
-      {cl with templval =
+    let cl = {cl with templval =
           { cl.templval with rebus = strip_params env sigma cl.templval.rebus };
         env = empty_env}
+    in
+    { hint_term = c; hint_type = cty; hint_uctx = ctx; hint_clnv = cl; hint_poly = poly }
   in
   let code = match p.code.obj with
-    | Res_pf c -> Res_pf (c, mk_clenv c)
-    | ERes_pf c -> ERes_pf (c, mk_clenv c)
+    | Res_pf c -> Res_pf (mk_clenv c)
+    | ERes_pf c -> ERes_pf (mk_clenv c)
     | Res_pf_THEN_trivial_fail c ->
-      Res_pf_THEN_trivial_fail (c, mk_clenv c)
-    | Give_exact c -> Give_exact (c, mk_clenv c)
+      Res_pf_THEN_trivial_fail (mk_clenv c)
+    | Give_exact c -> Give_exact (mk_clenv c)
     | Unfold_nth e -> Unfold_nth e
     | Extern t -> Extern t
   in
@@ -489,7 +496,6 @@ module Hint_db :
 sig
 type t
 val empty : ?name:hint_db_name -> TransparentState.t -> bool -> t
-val find : GlobRef.t -> t -> search_entry
 val map_none : secvars:Id.Pred.t -> t -> full_hint list
 val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list
 val map_existential : evar_map -> secvars:Id.Pred.t ->
@@ -800,9 +806,9 @@ let make_exact_entry env sigma info ~poly ?(name=PathAny) (c, cty, ctx) =
         | None -> pat
         in
         (Some hd,
-         { pri; poly; pat = Some pat; name;
+         { pri; pat = Some pat; name;
            db = None; secvars;
-           code = with_uid (Give_exact (c, cty, ctx)); })
+           code = with_uid (Give_exact (c, cty, ctx, poly)); })
 
 let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) (c, cty, ctx) =
   let cty = if hnf then hnf_constr env sigma cty else cty in
@@ -824,10 +830,10 @@ let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) (
     in
     if Int.equal nmiss 0 then
       (Some hd,
-       { pri; poly; pat = Some pat; name;
+       { pri; pat = Some pat; name;
          db = None;
          secvars;
-         code = with_uid (Res_pf(c,cty,ctx)); })
+         code = with_uid (Res_pf(c,cty,ctx,poly)); })
     else begin
       if not eapply then failwith "make_apply_entry";
       if verbose then begin
@@ -843,9 +849,9 @@ let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) (
         )
       end;
       (Some hd,
-       { pri; poly; pat = Some pat; name;
+       { pri; pat = Some pat; name;
          db = None; secvars;
-         code = with_uid (ERes_pf(c,cty,ctx)); })
+         code = with_uid (ERes_pf(c,cty,ctx,poly)); })
     end
   | _ -> failwith "make_apply_entry"
 
@@ -916,7 +922,6 @@ let make_unfold eref =
   let g = global_of_evaluable_reference eref in
   (Some g,
    { pri = 4;
-     poly = false;
      pat = None;
      name = PathHints [g];
      db = None;
@@ -927,7 +932,6 @@ let make_extern pri pat tacast =
   let hdconstr = Option.map try_head_pattern pat in
   (hdconstr,
    { pri = pri;
-     poly = false;
      pat = pat;
      name = PathAny;
      db = None;
@@ -954,12 +958,11 @@ let make_trivial env sigma poly ?(name=PathAny) r =
   let ce = mk_clenv_from_env env sigma None (c,t) in
   (Some hd,
    { pri=1;
-     poly = poly;
      pat = Some (Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma (clenv_type ce)));
      name = name;
      db = None;
      secvars = secvars_of_constr env sigma c;
-     code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) })
+     code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx,poly)) })
 
 
 
@@ -1070,29 +1073,30 @@ let subst_autohint (subst, obj) =
       (try head_constr_bound Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value)
        with Bound -> gr')
   in
+  let subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in
+  let subst_aux ((c, t, ctx, poly) as h) =
+    let c' = subst_mps subst c in
+    let t' = subst_mps subst t in
+    if c==c' && t'==t then h else (c', t', ctx, poly)
+  in
   let subst_hint (k,data as hint) =
     let k' = Option.Smart.map subst_key k in
     let env = Global.env () in
     let sigma = Evd.from_env env in
     let pat' = Option.Smart.map (subst_pattern env sigma subst) data.pat in
-    let subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in
     let code' = match data.code.obj with
-      | Res_pf (c,t,ctx) ->
-          let c' = subst_mps subst c in
-          let t' = subst_mps subst t in
-          if c==c' && t'==t then data.code.obj else Res_pf (c', t',ctx)
-      | ERes_pf (c,t,ctx) ->
-          let c' = subst_mps subst c in
-          let t' = subst_mps subst t in
-          if c==c' && t'==t then data.code.obj else ERes_pf (c',t',ctx)
-      | Give_exact (c,t,ctx) ->
-          let c' = subst_mps subst c in
-          let t' = subst_mps subst t in
-          if c==c' && t'== t then data.code.obj else Give_exact (c',t',ctx)
-      | Res_pf_THEN_trivial_fail (c,t,ctx) ->
-          let c' = subst_mps subst c in
-          let t' = subst_mps subst t in
-          if c==c' && t==t' then data.code.obj else Res_pf_THEN_trivial_fail (c',t',ctx)
+      | Res_pf h ->
+        let h' = subst_aux h in
+        if h == h' then data.code.obj else Res_pf h'
+      | ERes_pf h ->
+        let h' = subst_aux h in
+        if h == h' then data.code.obj else ERes_pf h'
+      | Give_exact h ->
+        let h' = subst_aux h in
+        if h == h' then data.code.obj else Give_exact h'
+      | Res_pf_THEN_trivial_fail h ->
+        let h' = subst_aux h in
+        if h == h' then data.code.obj else Res_pf_THEN_trivial_fail h'
       | Unfold_nth ref ->
           let ref' = subst_evaluable_reference subst ref in
           if ref==ref' then data.code.obj else Unfold_nth ref'
@@ -1336,6 +1340,9 @@ let constructor_hints env sigma eapply lems =
   List.map_append (fun (poly, lem) ->
       make_resolves env sigma (eapply,true,false) empty_hint_info ~check:true ~poly lem) lems
 
+let make_resolves env sigma info ~check ~poly ?name hint =
+  make_resolves env sigma (true, false, false) info ~check ~poly ?name hint
+
 let make_local_hint_db env sigma ts eapply lems =
   let map c = c env sigma in
   let lems = List.map map lems in
@@ -1365,13 +1372,13 @@ let make_db_list dbnames =
 (*                    Functions for printing the hints                    *)
 (**************************************************************************)
 
-let pr_hint_elt env sigma (c, _, _) = pr_econstr_env env sigma c
+let pr_hint_elt env sigma h = pr_econstr_env env sigma h.hint_term
 
 let pr_hint env sigma h = match h.obj with
-  | Res_pf (c, _) -> (str"simple apply " ++ pr_hint_elt env sigma c)
-  | ERes_pf (c, _) -> (str"simple eapply " ++ pr_hint_elt env sigma c)
-  | Give_exact (c, _) -> (str"exact " ++ pr_hint_elt env sigma c)
-  | Res_pf_THEN_trivial_fail (c, _) ->
+  | Res_pf c -> (str"simple apply " ++ pr_hint_elt env sigma c)
+  | ERes_pf c -> (str"simple eapply " ++ pr_hint_elt env sigma c)
+  | Give_exact c -> (str"exact " ++ pr_hint_elt env sigma c)
+  | Res_pf_THEN_trivial_fail c ->
       (str"simple apply " ++ pr_hint_elt env sigma c ++ str" ; trivial")
   | Unfold_nth c ->
     str"unfold " ++  pr_evaluable_reference c
@@ -1574,4 +1581,15 @@ let run_hint tac k = match warn_hint () with
     let info = Exninfo.reify () in
     Proofview.tclZERO ~info (UserError (None, (str "Tactic failure.")))
 
-let repr_hint h = h.obj
+module FullHint =
+struct
+  type t = full_hint
+  let priority (h : t) = h.pri
+  let pattern (h : t) = h.pat
+  let database (h : t) = h.db
+  let run (h : t) k = run_hint h.code k
+  let print env sigma (h : t) = pr_hint env sigma h.code
+  let name (h : t) = h.name
+
+  let repr (h : t) = h.code.obj
+end
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 6c8b7fed75..8243716624 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -15,7 +15,6 @@ open Environ
 open Evd
 open Tactypes
 open Clenv
-open Pattern
 open Typeclasses
 
 (** {6 General functions. } *)
@@ -40,8 +39,13 @@ type 'a hint_ast =
   | Unfold_nth of evaluable_global_reference       (* Hint Unfold *)
   | Extern     of Genarg.glob_generic_argument       (* Hint Extern *)
 
-type hint
-type raw_hint = constr * types * Univ.ContextSet.t
+type hint = {
+  hint_term : constr;
+  hint_type : types;
+  hint_uctx : Univ.ContextSet.t;
+  hint_clnv : clausenv;
+  hint_poly : bool;
+}
 
 type 'a hints_path_atom_gen =
   | PathHints of 'a list
@@ -51,26 +55,20 @@ type 'a hints_path_atom_gen =
 type hints_path_atom = GlobRef.t hints_path_atom_gen
 type hint_db_name = string
 
-type 'a with_metadata = private
-  { pri     : int
-  (** A number lower is higher priority *)
-  ; poly    : bool
-  (** Is the hint polymorpic and hence should be refreshed at each application *)
-  ; pat     : constr_pattern option
-  (** A pattern for the concl of the Goal *)
-  ; name    : hints_path_atom
-  (** A potential name to refer to the hint *)
-  ; db : string option
-  (** The database from which the hint comes *)
-  ; secvars : Id.Pred.t
-  (** The set of section variables the hint depends on *)
-  ; code    : 'a
-  (** the tactic to apply when the concl matches pat *)
-  }
-
-type full_hint = hint with_metadata
-
-type search_entry
+module FullHint :
+sig
+  type t
+  val priority : t -> int
+  val pattern : t -> Pattern.constr_pattern option
+  val database : t -> string option
+  val run : t -> (hint hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic
+  val name : t -> hints_path_atom
+  val print : env -> evar_map -> t -> Pp.t
+
+  (** This function is for backward compatibility only, not to use in newly
+    written code. *)
+  val repr : t -> hint hint_ast
+end
 
 (** The head may not be bound. *)
 
@@ -117,42 +115,41 @@ module Hint_db :
   sig
     type t
     val empty : ?name:hint_db_name -> TransparentState.t -> bool -> t
-    val find : GlobRef.t -> t -> search_entry
 
     (** All hints which have no pattern.
      * [secvars] represent the set of section variables that
      * can be used in the hint. *)
-    val map_none : secvars:Id.Pred.t -> t -> full_hint list
+    val map_none : secvars:Id.Pred.t -> t -> FullHint.t list
 
     (** All hints associated to the reference *)
-    val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list
+    val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> FullHint.t list
 
     (** All hints associated to the reference, respecting modes if evars appear in the
         arguments, _not_ using the discrimination net.
         Returns a [ModeMismatch] if there are declared modes and none matches.
         *)
     val map_existential : evar_map -> secvars:Id.Pred.t ->
-      (GlobRef.t * constr array) -> constr -> t -> full_hint list with_mode
+      (GlobRef.t * constr array) -> constr -> t -> FullHint.t list with_mode
 
     (** All hints associated to the reference, respecting modes if evars appear in the
         arguments and using the discrimination net.
         Returns a [ModeMismatch] if there are declared modes and none matches. *)
-    val map_eauto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> full_hint list with_mode
+    val map_eauto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> FullHint.t list with_mode
 
     (** All hints associated to the reference.
         Precondition: no evars should appear in the arguments, so no modes
         are checked. *)
     val map_auto : evar_map -> secvars:Id.Pred.t ->
-       (GlobRef.t * constr array) -> constr -> t -> full_hint list
+       (GlobRef.t * constr array) -> constr -> t -> FullHint.t list
 
     val add_one : env -> evar_map -> hint_entry -> t -> t
     val add_list : env -> evar_map -> hint_entry list -> t -> t
     val remove_one : GlobRef.t -> t -> t
     val remove_list : GlobRef.t list -> t -> t
     val iter : (GlobRef.t option ->
-                hint_mode array list -> full_hint list -> unit) -> t -> unit
+                hint_mode array list -> FullHint.t list -> unit) -> t -> unit
 
-    val fold : (GlobRef.t option -> hint_mode array list -> full_hint list -> 'a -> 'a) -> t -> 'a -> 'a
+    val fold : (GlobRef.t option -> hint_mode array list -> FullHint.t list -> 'a -> 'a) -> t -> 'a -> 'a
 
     val use_dn : t -> bool
     val transparent_state : t -> TransparentState.t
@@ -214,7 +211,7 @@ val prepare_hint : bool (* Check no remaining evars *) ->
          has missing arguments. *)
 
 val make_resolves :
-  env -> evar_map -> bool * bool * bool -> hint_info -> check:bool -> poly:bool -> ?name:hints_path_atom ->
+  env -> evar_map -> hint_info -> check:bool -> poly:bool -> ?name:hints_path_atom ->
   hint_term -> hint_entry list
 
 (** [make_resolve_hyp hname htyp].
@@ -225,19 +222,6 @@ val make_resolves :
 val make_resolve_hyp :
   env -> evar_map -> named_declaration -> hint_entry list
 
-(** [make_extern pri pattern tactic_expr] *)
-
-val make_extern :
-  int -> constr_pattern option -> Genarg.glob_generic_argument
-      -> hint_entry
-
-val run_hint : hint ->
-  ((raw_hint * clausenv) hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic
-
-(** This function is for backward compatibility only, not to use in newly
-    written code. *)
-val repr_hint : hint -> (raw_hint * clausenv) hint_ast
-
 (** Create a Hint database from the pairs (name, constr).
    Useful to take the current goal hypotheses as hints;
    Boolean tells if lemmas with evars are allowed *)
@@ -262,4 +246,3 @@ val pr_applicable_hint : Proof.t -> Pp.t
 val pr_hint_ref : env -> evar_map -> GlobRef.t -> Pp.t
 val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t
 val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t
-val pr_hint : env -> evar_map -> hint -> Pp.t