diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-07-03 13:32:50 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-07-03 13:32:50 +0200 |
commit | c17b3248f3473ec464ab19196558533f621d796c (patch) | |
tree | e3daa536a4db6f8fbd64a1c570f1f33a47302a3e /tactics/hints.mli | |
parent | 4deb788a24b50eec3da66ed32bb85c185123c007 (diff) | |
parent | bc5304a91cf4627063551422ad6e5a2cd1059897 (diff) |
Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commands
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 |