diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2017-03-30 16:28:21 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2018-07-02 16:27:18 +0200 |
| commit | 8d02317cc02ae5d007f5d2486d26bb37865ca0a9 (patch) | |
| tree | fb2951e3aee66c93f66c2bced46759a99baf3f46 /vernac/vernacexpr.ml | |
| parent | 02fe76c0c1c3f01c6fb4310dd4450b35f43005da (diff) | |
hints: add Hint Variables/Constants Opaque/Transparent commands
This gives user control on the transparent state of a hint db. Can
override defaults more easily (report by J. H. Jourdan).
For "core", declare that variables can be unfolded, but no constants
(ensures compatibility with previous auto which allowed conv on closed
terms)
Document Hint Variables
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 |