Wrap the content of full hints into a record.

7 files changed, 80 insertions, 63 deletions

diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index e365151079..db3631daa4 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -206,9 +206,9 @@ open Hints
 let extend_with_auto_hints env sigma l seq =
   let f (seq,sigma) p_a_t =
     match FullHint.repr p_a_t with
-    | Res_pf (c,_) | Give_exact (c,_)
-    | Res_pf_THEN_trivial_fail (c,_) ->
-      let (c, _, _) = c in
+    | 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 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)
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 33deefd0bd..9be58cb3fa 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
+  : poly:bool -> 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 : poly:bool -> 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 b435d560c7..fe7b62b316 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -144,11 +144,11 @@ let auto_unif_flags ?(allowed_evars = AllowAll) st =
     resolve_evars = false
 }
 
-let e_give_exact flags poly (c,clenv) =
+let e_give_exact flags poly 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
       let clenv', subst = Clenv.refresh_undefined_univs clenv in
@@ -173,17 +173,18 @@ 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 poly flags = begin fun gls (h, _) ->
+  let clenv', c = connect_hint_clenv ~poly 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 poly flags = begin fun gls (h, _) ->
+  let clenv', _ = connect_hint_clenv ~poly 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 poly 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
@@ -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 poly nprods h gl =
+  let { hint_term = c; hint_clnv = clenv } = 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 poly 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 poly 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 =
@@ -352,42 +355,42 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
       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 poly h
                           (fun gl clenv ->
                              matches_pattern concl p <*>
                                unify_resolve_refine poly 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 poly h (unify_resolve poly 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 poly h
                   (fun gl clenv ->
                              matches_pattern concl p <*>
                              unify_resolve_refine poly 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 poly h (unify_e_resolve poly 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 poly 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 poly h
+      | Res_pf_THEN_trivial_fail h ->
+         let fst = with_prods nprods poly h (unify_e_resolve poly 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
@@ -1248,7 +1251,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 } in
+    unify_e_resolve false 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 7a141bb53b..4a6364795b 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 poly 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 ~poly 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 poly 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 ~poly h gl in
     Tacticals.New.tclTHEN
     (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
     (e_give_exact c)
@@ -127,11 +127,11 @@ and e_my_find_search env sigma db_list local_db secvars concl =
       | _ -> 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 ~poly st h
+      | ERes_pf h -> unify_e_resolve poly st h
+      | Give_exact h -> e_exact poly st h
+      | Res_pf_THEN_trivial_fail h ->
+        Tacticals.New.tclTHEN (unify_e_resolve poly st h)
           (e_trivial_fail_db db_list local_db)
       | Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl
       | Extern tacast -> conclPattern concl (FullHint.pattern h) tacast
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 63ca4b8834..0a213d5d0e 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -137,7 +137,12 @@ type 'a with_uid = {
 
 type raw_hint = constr * types * Univ.ContextSet.t
 
-type hint = (raw_hint * clausenv) hint_ast with_uid
+type hint = {
+  hint_term : constr;
+  hint_type : types;
+  hint_uctx : Univ.ContextSet.t;
+  hint_clnv : clausenv;
+}
 
 type 'a with_metadata =
   { pri     : int
@@ -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
@@ -303,16 +308,18 @@ let instantiate_hint env sigma p =
   let mk_clenv (c, cty, ctx) =
     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; }
   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
@@ -1367,13 +1374,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
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 01b373b284..29fd90d3ef 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -39,7 +39,12 @@ type 'a hint_ast =
   | Unfold_nth of evaluable_global_reference       (* Hint Unfold *)
   | Extern     of Genarg.glob_generic_argument       (* Hint Extern *)
 
-type raw_hint = constr * types * Univ.ContextSet.t
+type hint = {
+  hint_term : constr;
+  hint_type : types;
+  hint_uctx : Univ.ContextSet.t;
+  hint_clnv : clausenv;
+}
 
 type 'a hints_path_atom_gen =
   | PathHints of 'a list
@@ -56,13 +61,13 @@ sig
   val is_polymorphic : t -> bool
   val pattern : t -> Pattern.constr_pattern option
   val database : t -> string option
-  val run : t -> ((raw_hint * clausenv) hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic
+  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 -> (raw_hint * clausenv) hint_ast
+  val repr : t -> hint hint_ast
 end
 
 (** The head may not be bound. *)