From 8d02317cc02ae5d007f5d2486d26bb37865ca0a9 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 30 Mar 2017 16:28:21 +0200 Subject: 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 --- vernac/classes.ml | 2 +- vernac/g_proofs.mlg | 8 ++++++-- vernac/ppvernac.ml | 5 ++++- vernac/vernacexpr.ml | 7 ++++++- 4 files changed, 17 insertions(+), 5 deletions(-) (limited to 'vernac') 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 -- cgit v1.2.3