From 55699e2b9a91356b7d43c4096f65fb199777b9a1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 8 Oct 2016 02:21:26 +0200 Subject: Fix bug #4958: [debug auto] should specify hint databases. --- tactics/hints.mli | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'tactics/hints.mli') diff --git a/tactics/hints.mli b/tactics/hints.mli index 6f5ee8ba5..411540aa1 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -43,11 +43,14 @@ type hints_path_atom = (* For forward hints, their names is the list of projections *) | PathAny +type hint_db_name = string + 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 *) name : hints_path_atom; (** A potential name to refer to the hint *) + db : hint_db_name option; code : 'a; (** the tactic to apply when the concl matches pat *) } @@ -77,7 +80,7 @@ val pp_hint_mode : hint_mode -> Pp.std_ppcmds module Hint_db : sig type t - val empty : transparent_state -> bool -> t + val empty : ?name:hint_db_name -> transparent_state -> bool -> t val find : global_reference -> t -> search_entry val map_none : t -> full_hint list @@ -113,8 +116,6 @@ module Hint_db : val unfolds : t -> Id.Set.t * Cset.t end -type hint_db_name = string - type hint_db = Hint_db.t type hnf = bool -- cgit v1.2.3