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 /vernac/vernacexpr.ml | |
parent | 4deb788a24b50eec3da66ed32bb85c185123c007 (diff) | |
parent | bc5304a91cf4627063551422ad6e5a2cd1059897 (diff) |
Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commands
Diffstat (limited to 'vernac/vernacexpr.ml')
-rw-r--r-- | vernac/vernacexpr.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index f74383b02..f5f37339c 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -121,12 +121,17 @@ type 'a hint_info_gen = 'a Typeclasses.hint_info_gen = type hint_info_expr = Hints.hint_info_expr [@@ocaml.deprecated "Please use [Hints.hint_info_expr]"] +type 'a hints_transparency_target = 'a Hints.hints_transparency_target = + | HintsVariables + | HintsConstants + | HintsReferences of 'a list + type hints_expr = Hints.hints_expr = | HintsResolve of (Hints.hint_info_expr * bool * Hints.reference_or_constr) list | HintsResolveIFF of bool * qualid list * int option | HintsImmediate of Hints.reference_or_constr list | HintsUnfold of qualid list - | HintsTransparency of qualid list * bool + | HintsTransparency of qualid hints_transparency_target * bool | HintsMode of qualid * Hints.hint_mode list | HintsConstructors of qualid list | HintsExtern of int * constr_expr option * Genarg.raw_generic_argument |