diff options
| author |  Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-06-27 17:40:48 +0000 |
|---|---|---|
| committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-07-03 16:10:19 +0000 |
| commit | f0e546fdb98ff7244d5c393c739f5b7238295918 (patch) | |
| tree | 6b50e480a26cb981d16a5e575fbee9100fe1dbe1 /vernac/vernacinterp.ml | |
| parent | d3127693d4a2125088aa512f593d782843482f2a (diff) | |
[vernac] use a record for the contents of the “deprecated” attribute
Diffstat (limited to 'vernac/vernacinterp.ml')
| -rw-r--r-- | vernac/vernacinterp.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 30c1ddbfd..1bb1414f3 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -12,14 +12,17 @@ open Util open Pp open CErrors -type deprecation = bool +type deprecation = { since : string option ; note : string option } + +let mk_deprecation ?(since=None) ?(note=None) () = + { since ; note } type atts = { loc : Loc.t option; locality : bool option; polymorphic : bool; program : bool; - deprecated : (string * string) option; + deprecated : deprecation option; } let mk_atts ?(loc=None) ?(locality=None) ?(polymorphic=false) ?(program=false) ?(deprecated=None) () : atts = @@ -32,7 +35,7 @@ type plugin_args = Genarg.raw_generic_argument list (* Table of vernac entries *) let vernac_tab = (Hashtbl.create 211 : - (Vernacexpr.extend_name, deprecation * plugin_args vernac_command) Hashtbl.t) + (Vernacexpr.extend_name, bool * plugin_args vernac_command) Hashtbl.t) let vinterp_add depr s f = try |