diff options
| author | Vincent Laporte | 2018-12-06 09:07:24 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-12-06 09:07:24 +0000 |
| commit | a2c8b7df8a0702ab716c0b97ad63d235b58b93a0 (patch) | |
| tree | c3320b64340018f5a73d111c3fefc79b4c507741 /vernac/attributes.ml | |
| parent | 5331889da2d3f57f7aed935f6456e39765eb8b31 (diff) | |
| parent | 90ae85437a281ca655f7e9511ef09874ba591857 (diff) | |
Merge PR #8917: Small cleanup wrt attributes_of_flags and template attribute
Diffstat (limited to 'vernac/attributes.ml')
| -rw-r--r-- | vernac/attributes.ml | 19 |
1 files changed, 2 insertions, 17 deletions
diff --git a/vernac/attributes.ml b/vernac/attributes.ml index 75ca027332..4f238f38e6 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -78,14 +78,6 @@ type deprecation = { since : string option ; note : string option } let mk_deprecation ?(since=None) ?(note=None) () = { since ; note } -type t = { - locality : bool option; - polymorphic : bool; - template : bool option; - program : bool; - deprecated : deprecation option; -} - let assert_empty k v = if v <> VernacFlagEmpty then user_err Pp.(str "Attribute " ++ str k ++ str " does not accept arguments") @@ -181,10 +173,9 @@ let polymorphic_nowarn = universe_transform ~warn_unqualified:false >> qualify_attribute ukey polymorphic_base -let universe_poly_template = - let template = bool_attribute ~name:"Template" ~on:"template" ~off:"notemplate" in +let template = universe_transform ~warn_unqualified:true >> - qualify_attribute ukey (polymorphic_base ++ template) + qualify_attribute ukey (bool_attribute ~name:"Template" ~on:"template" ~off:"notemplate") let polymorphic = universe_transform ~warn_unqualified:true >> @@ -207,12 +198,6 @@ let deprecation_parser : deprecation key_parser = fun orig args -> let deprecation = attribute_of_list ["deprecated",deprecation_parser] -let attributes_of_flags f = - let ((locality, deprecated), (polymorphic, template)), program = - parse (locality ++ deprecation ++ universe_poly_template ++ program) f - in - { polymorphic; program; locality; template; deprecated } - let only_locality atts = parse locality atts let only_polymorphism atts = parse polymorphic atts |