Imported Upstream version 8.5~beta3+dfsg

1 files changed, 21 insertions, 18 deletions

diff --git a/tactics/hints.mli b/tactics/hints.mli
index 958cca1c..3a0521f6 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,14 @@ 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 raw_hint = constr * types * Univ.universe_context_set
 
 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 +51,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
 
@@ -69,6 +70,7 @@ type hints_path =
 val normalize_path : hints_path -> hints_path
 val path_matches : hints_path -> hints_path_atom list -> bool
 val path_derivate : hints_path -> hints_path_atom -> hints_path
+val pp_hints_path_atom : hints_path_atom -> Pp.std_ppcmds
 val pp_hints_path : hints_path -> Pp.std_ppcmds
 
 module Hint_db :
@@ -76,28 +78,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 add_one : env -> evar_map -> hint_entry -> t -> t
+    val add_list : env -> evar_map -> 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
@@ -151,8 +153,9 @@ val interp_hints : polymorphic -> hints_expr -> hints_entry
 
 val add_hints : locality_flag -> hint_db_name list -> hints_entry -> unit
 
-val prepare_hint : bool (* Check no remaining evars *) -> env -> evar_map -> 
-  open_constr -> hint_term
+val prepare_hint : bool (* Check no remaining evars *) ->
+  (bool * bool) (* polymorphic or monomorphic, local or global *) ->
+  env -> evar_map -> open_constr -> hint_term
 
 (** [make_exact_entry pri (c, ctyp)].
    [c] is the term given as an exact proof to solve the goal;
@@ -197,12 +200,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 ->
+  ((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_auto_tactic : 'a auto_tactic -> 'a auto_tactic_ast
+val repr_hint : hint -> (raw_hint * clausenv) hint_ast
 
 val extern_intern_tac :
   (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) Hook.t
@@ -227,7 +230,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 *)