Opacify the type of hint metadata.

6 files changed, 62 insertions, 53 deletions

diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 3dd5059e5d..e365151079 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -205,7 +205,7 @@ 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
+    match FullHint.repr p_a_t with
     | Res_pf (c,_) | Give_exact (c,_)
     | Res_pf_THEN_trivial_fail (c,_) ->
       let (c, _, _) = c in
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 681c4e910f..a73db95884 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
@@ -381,7 +381,8 @@ 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 poly = FullHint.is_polymorphic h in
   let tactic = function
     | Res_pf (c,cl) -> unify_resolve_gen ~poly flags (c,cl)
     | ERes_pf _ -> Proofview.Goal.enter (fun gl ->
@@ -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/class_tactics.ml b/tactics/class_tactics.ml
index 18994d0242..2c9d06f5b9 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -346,7 +346,12 @@ 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 poly = FullHint.is_polymorphic h in
+      let p = FullHint.pattern h in
+      let secvars = FullHint.secvars h in (* The use below looks suspicious *)
+      let name = FullHint.name h in
       let tac = function
         | Res_pf (term,cl) ->
            if get_typeclasses_filtered_unification () then
@@ -391,7 +396,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 +404,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
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index c2eabffd44..7a141bb53b 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -120,10 +120,11 @@ 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 poly = FullHint.is_polymorphic h in
+      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)
@@ -133,10 +134,10 @@ and e_my_find_search env sigma db_list local_db secvars concl =
         Tacticals.New.tclTHEN (unify_e_resolve poly st (term,cl))
           (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 9595fa2033..78ed81ec37 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1576,4 +1576,17 @@ 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 is_polymorphic (h : t) = h.poly
+  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 secvars (h : t) = h.secvars
+
+  let repr (h : t) = h.code.obj
+end
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 56bd6fad44..4e7abad2b6 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,7 +39,6 @@ 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 'a hints_path_atom_gen =
@@ -51,24 +49,22 @@ 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
+module FullHint :
+sig
+  type t
+  val priority : t -> int
+  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 name : t -> hints_path_atom
+  val secvars : t -> Id.Pred.t
+  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
+end
 
 (** The head may not be bound. *)
 
@@ -119,37 +115,37 @@ module Hint_db :
     (** 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
@@ -222,13 +218,6 @@ val make_resolves :
 val make_resolve_hyp :
   env -> evar_map -> named_declaration -> hint_entry list
 
-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 *)
@@ -253,4 +242,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