diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-11-30 16:23:38 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-11-30 16:23:38 +0100 |
| commit | 1099b748bb080d449037fbd06199c012fa3ce387 (patch) | |
| tree | 505ca1d6ba1c2fd7be8a75111a2e8f79fbfbc59d /tactics/hints.mli | |
| parent | 3e6fa1cbdc0ec145728089000595b6ea29f37a4c (diff) | |
Fix bug #5232: proper globalization of hints paths
Diffstat (limited to 'tactics/hints.mli')
| -rw-r--r-- | tactics/hints.mli | 25 |
1 files changed, 17 insertions, 8 deletions
diff --git a/tactics/hints.mli b/tactics/hints.mli index 42a2896ed..1be3e0c52 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -42,11 +42,12 @@ type 'a hint_ast = type hint type raw_hint = constr * types * Univ.universe_context_set -type hints_path_atom = - | PathHints of global_reference list +type 'a hints_path_atom_gen = + | PathHints of 'a list (* For forward hints, their names is the list of projections *) | PathAny +type hints_path_atom = global_reference hints_path_atom_gen type hint_db_name = string type 'a with_metadata = private { @@ -67,20 +68,28 @@ type search_entry type hint_entry -type hints_path = - | PathAtom of hints_path_atom - | PathStar of hints_path - | PathSeq of hints_path * hints_path - | PathOr of hints_path * hints_path +type 'a hints_path_gen = + | PathAtom of 'a hints_path_atom_gen + | PathStar of 'a hints_path_gen + | PathSeq of 'a hints_path_gen * 'a hints_path_gen + | PathOr of 'a hints_path_gen * 'a hints_path_gen | PathEmpty | PathEpsilon +type pre_hints_path = Libnames.reference hints_path_gen +type hints_path = global_reference hints_path_gen + 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_gen : ('a -> Pp.std_ppcmds) -> 'a hints_path_gen -> Pp.std_ppcmds +val pp_hints_path_atom : ('a -> Pp.std_ppcmds) -> 'a hints_path_atom_gen -> Pp.std_ppcmds val pp_hints_path : hints_path -> Pp.std_ppcmds val pp_hint_mode : hint_mode -> Pp.std_ppcmds +val glob_hints_path_atom : + Libnames.reference hints_path_atom_gen -> Globnames.global_reference hints_path_atom_gen +val glob_hints_path : + Libnames.reference hints_path_gen -> Globnames.global_reference hints_path_gen module Hint_db : sig |