[vernac] use a record for the contents of the “deprecated” attribute

3 files changed, 20 insertions, 8 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 080d42607..27f2a740e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2352,7 +2352,14 @@ let attributes_of_flags f atts =
            begin match v with
              | VernacFlagList [ "since", VernacFlagLeaf since ; "note", VernacFlagLeaf note ]
              | VernacFlagList [ "note", VernacFlagLeaf note ; "since", VernacFlagLeaf since ] ->
-               (polymorphism, { atts with deprecated = Some (since, note) })
+               let since = Some since and note = Some note in
+               (polymorphism, { atts with deprecated = Some (mk_deprecation ~since ~note ()) })
+             | VernacFlagList [ "since", VernacFlagLeaf since ] ->
+               let since = Some since in
+               (polymorphism, { atts with deprecated = Some (mk_deprecation ~since ()) })
+             | VernacFlagList [ "note", VernacFlagLeaf note ] ->
+               let note = Some note in
+               (polymorphism, { atts with deprecated = Some (mk_deprecation ~note ()) })
              |  _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute")
            end
        | "deprecated" ->
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
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index 362c05d4c..46468b309 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -10,25 +10,27 @@
 
 (** Interpretation of extended vernac phrases. *)
 
-type deprecation = bool
+type deprecation = { since : string option ; note : string option }
+
+val mk_deprecation : ?since: string option -> ?note: string option -> unit -> deprecation
 
 type atts = {
   loc : Loc.t option;
   locality : bool option;
   polymorphic : bool;
   program : bool;
-  deprecated : (string * string) option; (* Since, Note *)
+  deprecated : deprecation option;
 }
 
 val mk_atts : ?loc: Loc.t option -> ?locality: bool option ->
-  ?polymorphic: bool -> ?program: bool -> ?deprecated: (string * string) option -> unit -> atts
+  ?polymorphic: bool -> ?program: bool -> ?deprecated: deprecation option -> unit -> atts
 
 type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
 
 type plugin_args = Genarg.raw_generic_argument list
 
 val vinterp_init : unit -> unit
-val vinterp_add : deprecation -> Vernacexpr.extend_name -> plugin_args vernac_command -> unit
+val vinterp_add : bool -> Vernacexpr.extend_name -> plugin_args vernac_command -> unit
 val overwriting_vinterp_add : Vernacexpr.extend_name -> plugin_args vernac_command -> unit
 
 val call : Vernacexpr.extend_name -> plugin_args -> atts:atts -> st:Vernacstate.t -> Vernacstate.t