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 | |
| parent | 4deb788a24b50eec3da66ed32bb85c185123c007 (diff) | |
| parent | bc5304a91cf4627063551422ad6e5a2cd1059897 (diff) | |
Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commands
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/classes.ml | 2 | ||||
| -rw-r--r-- | vernac/g_proofs.mlg | 8 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 5 | ||||
| -rw-r--r-- | vernac/vernacexpr.ml | 7 |
4 files changed, 17 insertions, 5 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 26d105ecf..bf734ab36 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -42,7 +42,7 @@ let typeclasses_db = "typeclass_instances" let set_typeclass_transparency c local b = Hints.add_hints ~local [typeclasses_db] - (Hints.HintsTransparencyEntry ([c], b)) + (Hints.HintsTransparencyEntry (Vernacexpr.HintsReferences [c], b)) let _ = Hook.set Typeclasses.add_instance_hint_hook diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index 72db53f68..cccdbfc91 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -117,8 +117,12 @@ GRAMMAR EXTEND Gram | IDENT "Resolve"; "<-"; lc = LIST1 global; n = OPT natural -> { HintsResolveIFF (false, lc, n) } | IDENT "Immediate"; lc = LIST1 reference_or_constr -> { HintsImmediate lc } - | IDENT "Transparent"; lc = LIST1 global -> { HintsTransparency (lc, true) } - | IDENT "Opaque"; lc = LIST1 global -> { HintsTransparency (lc, false) } + | IDENT "Variables"; IDENT "Transparent" -> { HintsTransparency (HintsVariables, true) } + | IDENT "Variables"; IDENT "Opaque" -> { HintsTransparency (HintsVariables, false) } + | IDENT "Constants"; IDENT "Transparent" -> { HintsTransparency (HintsConstants, true) } + | IDENT "Constants"; IDENT "Opaque" -> { HintsTransparency (HintsConstants, false) } + | IDENT "Transparent"; lc = LIST1 global -> { HintsTransparency (HintsReferences lc, true) } + | IDENT "Opaque"; lc = LIST1 global -> { HintsTransparency (HintsReferences lc, false) } | IDENT "Mode"; l = global; m = mode -> { HintsMode (l, m) } | IDENT "Unfold"; lqid = LIST1 global -> { HintsUnfold lqid } | IDENT "Constructors"; lc = LIST1 global -> { HintsConstructors lc } ] ] diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 56dfaa54a..5fbe1f4e4 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -210,7 +210,10 @@ open Pputils | HintsTransparency (l, b) -> keyword (if b then "Transparent" else "Opaque") ++ spc () - ++ prlist_with_sep sep pr_qualid l + ++ (match l with + | HintsVariables -> keyword "Variables" + | HintsConstants -> keyword "Constants" + | HintsReferences l -> prlist_with_sep sep pr_qualid l) | HintsMode (m, l) -> keyword "Mode" ++ spc () 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 |