diff options
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 |