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

1 files changed, 8 insertions, 1 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" ->