From d3127693d4a2125088aa512f593d782843482f2a Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Mon, 25 Jun 2018 16:09:11 +0000 Subject: [vernac] use plain strings as attribute names The concrete syntax is still restricted to identifiers. --- vernac/vernacentries.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'vernac/vernacentries.ml') diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e61687290..080d42607 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2326,7 +2326,6 @@ let attributes_of_flags f atts = in List.fold_left (fun (polymorphism, atts) (k, v) -> - let k = Names.Id.to_string k in match k with | "program" when not atts.program -> assert_empty k v; @@ -2351,8 +2350,8 @@ let attributes_of_flags f atts = user_err Pp.(str "Locality specified twice") | "deprecated" when Option.is_empty atts.deprecated -> begin match v with - | VernacFlagList [ k1, VernacFlagLeaf since ; k2, VernacFlagLeaf note ] - when Names.Id.(equal k1 (of_string "since") && equal k2 (of_string "note")) -> + | VernacFlagList [ "since", VernacFlagLeaf since ; "note", VernacFlagLeaf note ] + | VernacFlagList [ "note", VernacFlagLeaf note ; "since", VernacFlagLeaf since ] -> (polymorphism, { atts with deprecated = Some (since, note) }) | _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute") end -- cgit v1.2.3