diff options
| author | Maxime Dénès | 2019-05-16 18:20:07 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-06-06 08:54:39 +0200 |
| commit | fb30e8880a3027ef1c957df668a906d723e8a8a0 (patch) | |
| tree | ad2825c374340dfa0bb4c8785034e689c0311d61 /vernac/attributes.ml | |
| parent | c0a695e89b0562eb6450c04ddba5e6e0414e5fd8 (diff) | |
`deprecated` attribute support for notations and syntactic definitions
We also slightly change the semantics of the `compat` syntax modifier to
re-express it in terms of the `deprecated` attribute, and we deprecate
it in favor of the latter.
Diffstat (limited to 'vernac/attributes.ml')
| -rw-r--r-- | vernac/attributes.ml | 16 |
1 files changed, 4 insertions, 12 deletions
diff --git a/vernac/attributes.ml b/vernac/attributes.ml index 1ad5862d5d..ab14974598 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -73,11 +73,6 @@ module Notations = struct end open Notations -type deprecation = { since : string option ; note : string option } - -let mk_deprecation ?(since=None) ?(note=None) () = - { since ; note } - let assert_empty k v = if v <> VernacFlagEmpty then user_err Pp.(str "Attribute " ++ str k ++ str " does not accept arguments") @@ -213,19 +208,16 @@ let polymorphic = universe_transform ~warn_unqualified:true >> qualify_attribute ukey polymorphic_base -let deprecation_parser : deprecation key_parser = fun orig args -> +let deprecation_parser : Deprecation.t key_parser = fun orig args -> assert_once ~name:"deprecation" orig; match args with | VernacFlagList [ "since", VernacFlagLeaf since ; "note", VernacFlagLeaf note ] | VernacFlagList [ "note", VernacFlagLeaf note ; "since", VernacFlagLeaf since ] -> - let since = Some since and note = Some note in - mk_deprecation ~since ~note () + Deprecation.make ~since ~note () | VernacFlagList [ "since", VernacFlagLeaf since ] -> - let since = Some since in - mk_deprecation ~since () + Deprecation.make ~since () | VernacFlagList [ "note", VernacFlagLeaf note ] -> - let note = Some note in - mk_deprecation ~note () + Deprecation.make ~note () | _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute") let deprecation = attribute_of_list ["deprecated",deprecation_parser] |