From f0e546fdb98ff7244d5c393c739f5b7238295918 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Wed, 27 Jun 2018 17:40:48 +0000 Subject: [vernac] use a record for the contents of the “deprecated” attribute MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- vernac/vernacinterp.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'vernac/vernacinterp.ml') 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 -- cgit v1.2.3