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/vernacentries.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'vernac/vernacentries.ml') 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" -> -- cgit v1.2.3