diff options
Diffstat (limited to 'tactics/hints.mli')
| -rw-r--r-- | tactics/hints.mli | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/tactics/hints.mli b/tactics/hints.mli index ca18f835a..9bf6c175a 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -81,12 +81,17 @@ type hint_mode = | ModeNoHeadEvar (* No evar at the head *) | ModeOutput (* Anything *) +type 'a hints_transparency_target = + | HintsVariables + | HintsConstants + | HintsReferences of 'a list + type hints_expr = | HintsResolve of (hint_info_expr * bool * reference_or_constr) list | HintsResolveIFF of bool * Libnames.qualid list * int option | HintsImmediate of reference_or_constr list | HintsUnfold of Libnames.qualid list - | HintsTransparency of Libnames.qualid list * bool + | HintsTransparency of Libnames.qualid hints_transparency_target * bool | HintsMode of Libnames.qualid * hint_mode list | HintsConstructors of Libnames.qualid list | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument @@ -173,7 +178,7 @@ type hints_entry = | HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list | HintsCutEntry of hints_path | HintsUnfoldEntry of evaluable_global_reference list - | HintsTransparencyEntry of evaluable_global_reference list * bool + | HintsTransparencyEntry of evaluable_global_reference hints_transparency_target * bool | HintsModeEntry of GlobRef.t * hint_mode list | HintsExternEntry of hint_info * Genarg.glob_generic_argument |