Rationalizing a bit the interface of Hints.

6 files changed, 36 insertions, 36 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 7da841571..72ba9e0bd 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -377,7 +377,7 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly}))
     | Extern tacast -> 
       conclPattern concl p tacast
   in
-  tclLOG dbg (fun () -> pr_autotactic t) (run_auto_tactic t tactic)
+  tclLOG dbg (fun () -> pr_hint t) (run_hint t tactic)
 
 and trivial_resolve dbg mod_delta db_list local_db cl =
   try
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 0cc8a0b1b..8dacc1362 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -19,7 +19,7 @@ val extern_interp :
 
 (** Auto and related automation tactics *)
 
-val priority : ('a * pri_auto_tactic) list -> ('a * pri_auto_tactic) list
+val priority : ('a * full_hint) list -> ('a * full_hint) list
 
 val default_search_depth : int ref
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index e11458c04..6ea25269c 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -231,13 +231,13 @@ and e_my_find_search db_list local_db hdc complete sigma concl =
       | Unfold_nth c -> Proofview.V82.tactic (tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c]))
       | Extern tacast -> conclPattern concl p tacast
       in
-      let tac = Proofview.V82.of_tactic (run_auto_tactic t tac) in
+      let tac = Proofview.V82.of_tactic (run_hint t tac) in
       let tac = if complete then tclCOMPLETE tac else tac in
-	match repr_auto_tactic t with
-	| Extern _ -> (tac,b,true, name, lazy (pr_autotactic t))
+	match repr_hint t with
+	| Extern _ -> (tac,b,true, name, lazy (pr_hint t))
 	| _ ->
 (* 	  let tac gl = with_pattern (pf_env gl) (project gl) flags p concl tac gl in *)
-	    (tac,b,false, name, lazy (pr_autotactic t))
+	    (tac,b,false, name, lazy (pr_hint t))
   in List.map tac_of_hint hintl
 
 and e_trivial_resolve db_list local_db sigma concl =
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index d738677e5..50925ecde 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -172,8 +172,8 @@ and e_my_find_search db_list local_db hdc concl =
         | Unfold_nth c -> Proofview.V82.tactic (reduce (Unfold [AllOccurrences,c]) onConcl)
         | Extern tacast -> conclPattern concl p tacast
        in
-       let tac = Proofview.V82.of_tactic (run_auto_tactic t tac) in
-       (tac, lazy (pr_autotactic t)))
+       let tac = Proofview.V82.of_tactic (run_hint t tac) in
+       (tac, lazy (pr_hint t)))
   in
   List.map tac_of_hint hintl
 
diff --git a/tactics/hints.ml b/tactics/hints.ml
index f83aa5601..b8e4dd9fa 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -68,7 +68,7 @@ let decompose_app_bound t =
 (*           The Type of Constructions Autotactic Hints                 *)
 (************************************************************************)
 
-type 'a auto_tactic_ast =
+type 'a hint_ast =
   | Res_pf     of 'a (* Hint Apply *)
   | ERes_pf    of 'a (* Hint EApply *)
   | Give_exact of 'a
@@ -92,9 +92,9 @@ type hint_term =
   | IsGlobRef of global_reference
   | IsConstr of constr * Univ.universe_context_set
 
-type 'a auto_tactic = 'a auto_tactic_ast
+type hint = (constr * clausenv) hint_ast
 
-type 'a gen_auto_tactic = {
+type 'a with_metadata = {
   pri  : int;            (* A number lower is higher priority *)
   poly  : polymorphic;    (** Is the hint polymorpic and hence should be refreshed at each application *)
   pat  : constr_pattern option; (* A pattern for the concl of the Goal *)
@@ -102,13 +102,13 @@ type 'a gen_auto_tactic = {
   code : 'a     (* the tactic to apply when the concl matches pat *)
 }
 
-type pri_auto_tactic = (constr * clausenv) auto_tactic gen_auto_tactic
+type full_hint = hint with_metadata
 
 type hint_entry = global_reference option * 
-  (constr * types * Univ.universe_context_set) auto_tactic_ast gen_auto_tactic
+  (constr * types * Univ.universe_context_set) hint_ast with_metadata
 
-let run_auto_tactic tac k = k tac
-let repr_auto_tactic tac = tac
+let run_hint tac k = k tac
+let repr_hint h = h
 
 let eq_hints_path_atom p1 p2 = match p1, p2 with
 | PathHints gr1, PathHints gr2 -> List.equal eq_gr gr1 gr2
@@ -125,7 +125,7 @@ let eq_auto_tactic t1 t2 = match t1, t2 with
 | (Res_pf _ | ERes_pf _ | Give_exact _ | Res_pf_THEN_trivial_fail _
   | Unfold_nth _ | Extern _), _ -> false
 
-let eq_gen_auto_tactic t1 t2 =
+let eq_hint_metadata t1 t2 =
   Int.equal t1.pri t2.pri &&
   Option.equal constr_pattern_eq t1.pat t2.pat &&
   eq_hints_path_atom t1.name t2.name &&
@@ -153,7 +153,7 @@ let pri_order t1 t2 = pri_order_int t1 t2 <= 0
      - un discrimination net borné (Btermdn.t) constitué de tous les
        patterns de la seconde liste de tactiques *)
 
-type stored_data = int * pri_auto_tactic
+type stored_data = int * full_hint
     (* First component is the index of insertion in the table, to keep most recent first semantics. *)
 
 module Bounded_net = Btermdn.Make(struct
@@ -481,7 +481,7 @@ module Hint_db = struct
       match k with
       | None ->
           (** ppedrot: this equality here is dubious. Maybe we can remove it? *)
-          let is_present (_, (_, v')) = eq_gen_auto_tactic v v' in
+          let is_present (_, (_, v')) = eq_hint_metadata v v' in
 	  if not (List.exists is_present db.hintdb_nopat) then
 	    (** FIXME *)
 	    { db with hintdb_nopat = (gr,idv) :: db.hintdb_nopat }
@@ -1146,7 +1146,7 @@ let make_db_list dbnames =
 (*                    Functions for printing the hints                    *)
 (**************************************************************************)
 
-let pr_autotactic =
+let pr_hint =
   function
   | Res_pf (c,clenv) -> (str"apply " ++ pr_constr c)
   | ERes_pf (c,clenv) -> (str"eapply " ++ pr_constr c)
@@ -1163,11 +1163,11 @@ let pr_autotactic =
       in
       (str "(*external*) " ++ Pptactic.pr_glob_tactic env tac)
 
-let pr_hint (id, v) =
-  (pr_autotactic v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ())
+let pr_id_hint (id, v) =
+  (pr_hint v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ())
 
 let pr_hint_list hintlist =
-  (str "  " ++ hov 0 (prlist pr_hint hintlist) ++ fnl ())
+  (str "  " ++ hov 0 (prlist pr_id_hint hintlist) ++ fnl ())
 
 let pr_hints_db (name,db,hintlist) =
   (str "In the database " ++ str name ++ str ":" ++
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 958cca1c3..687bc78c7 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -28,7 +28,7 @@ val decompose_app_bound : constr -> global_reference * constr array
 
 (** Pre-created hint databases *)
 
-type 'a auto_tactic_ast =
+type 'a hint_ast =
   | Res_pf     of 'a (* Hint Apply *)
   | ERes_pf    of 'a (* Hint EApply *)
   | Give_exact of 'a
@@ -36,13 +36,13 @@ type 'a auto_tactic_ast =
   | Unfold_nth of evaluable_global_reference       (* Hint Unfold *)
   | Extern     of Tacexpr.glob_tactic_expr       (* Hint Extern *)
 
-type 'a auto_tactic
+type hint
 
 type hints_path_atom = 
   | PathHints of global_reference list
   | PathAny
 
-type 'a gen_auto_tactic = private {
+type 'a with_metadata = private {
   pri   : int;            (** A number between 0 and 4, 4 = lower priority *)
   poly  : polymorphic;    (** Is the hint polymorpic and hence should be refreshed at each application *)
   pat   : constr_pattern option; (** A pattern for the concl of the Goal *)
@@ -50,7 +50,7 @@ type 'a gen_auto_tactic = private {
   code  : 'a; (** the tactic to apply when the concl matches pat *)
 }
 
-type pri_auto_tactic = (constr * clausenv) auto_tactic gen_auto_tactic
+type full_hint = hint with_metadata
 
 type search_entry
 
@@ -76,28 +76,28 @@ module Hint_db :
     type t
     val empty : transparent_state -> bool -> t
     val find : global_reference -> t -> search_entry
-    val map_none : t -> pri_auto_tactic list
+    val map_none : t -> full_hint list
 
     (** All hints associated to the reference *)
-    val map_all : global_reference -> t -> pri_auto_tactic list
+    val map_all : global_reference -> t -> full_hint list
 
     (** All hints associated to the reference, respecting modes if evars appear in the 
 	arguments, _not_ using the discrimination net. *)
-    val map_existential : (global_reference * constr array) -> constr -> t -> pri_auto_tactic list
+    val map_existential : (global_reference * constr array) -> constr -> t -> full_hint list
 
     (** All hints associated to the reference, respecting modes if evars appear in the 
 	arguments and using the discrimination net. *)
-    val map_eauto : (global_reference * constr array) -> constr -> t -> pri_auto_tactic list
+    val map_eauto : (global_reference * constr array) -> constr -> t -> full_hint list
 
     (** All hints associated to the reference, respecting modes if evars appear in the 
 	arguments. *)
-    val map_auto : (global_reference * constr array) -> constr -> t -> pri_auto_tactic list
+    val map_auto : (global_reference * constr array) -> constr -> t -> full_hint list
 
     val add_one : hint_entry -> t -> t
     val add_list : (hint_entry) list -> t -> t
     val remove_one : global_reference -> t -> t
     val remove_list : global_reference list -> t -> t
-    val iter : (global_reference option -> bool array list -> pri_auto_tactic list -> unit) -> t -> unit
+    val iter : (global_reference option -> bool array list -> full_hint list -> unit) -> t -> unit
 
     val use_dn : t -> bool
     val transparent_state : t -> transparent_state
@@ -197,12 +197,12 @@ val make_extern :
   int -> constr_pattern option -> Tacexpr.glob_tactic_expr
       -> hint_entry
 
-val run_auto_tactic : 'a auto_tactic ->
-  ('a auto_tactic_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic
+val run_hint : hint ->
+  ((constr * 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_auto_tactic : 'a auto_tactic -> 'a auto_tactic_ast
+val repr_hint : hint -> (constr * clausenv) hint_ast
 
 val extern_intern_tac :
   (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) Hook.t
@@ -227,7 +227,7 @@ val pr_applicable_hint : unit -> std_ppcmds
 val pr_hint_ref : global_reference -> std_ppcmds
 val pr_hint_db_by_name : hint_db_name -> std_ppcmds
 val pr_hint_db : Hint_db.t -> std_ppcmds
-val pr_autotactic : (constr * 'a) auto_tactic -> Pp.std_ppcmds
+val pr_hint : hint -> Pp.std_ppcmds
 
 (** Hook for changing the initialization of auto *)