diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-12 21:14:07 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-12 21:14:07 +0200 |
commit | 05ad4f49ac2203dd64dfec79a1fc62ee52115724 (patch) | |
tree | 920faae7946821c093345fd1804c40336bd9f1c4 /tactics/hints.mli | |
parent | 8a6c792505160de4ba2123ef049ab45d28873e47 (diff) | |
parent | 0222f685ebdd55a1596d6689b96ebb86454ba1a7 (diff) |
Merge branch 'v8.6'
Diffstat (limited to 'tactics/hints.mli')
-rw-r--r-- | tactics/hints.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/tactics/hints.mli b/tactics/hints.mli index 9a3817203..48351a317 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -46,11 +46,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 *) } @@ -80,7 +83,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 @@ -116,8 +119,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 |