diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-12-07 12:28:14 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-12-07 12:28:14 +0100 |
| commit | ad768e435a736ca51ac79a575967b388b34918c7 (patch) | |
| tree | 6f87c9bc585d15862b66c39feb3a5172e468f67f /tactics/hints.mli | |
| parent | cf8ecf83b5cc52f7ea73dc1d3af59bf03deff688 (diff) | |
| parent | 40cffd816b7adbf8f136f62f6f891fb5be9b96a6 (diff) | |
Merge branch 'v8.6'
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 73cafbefd..05d41adfe 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -45,11 +45,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 { @@ -70,20 +71,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 |