diff options
| author |  Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-06-25 16:09:11 +0000 |
|---|---|---|
| committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-07-03 16:10:16 +0000 |
| commit | d3127693d4a2125088aa512f593d782843482f2a (patch) | |
| tree | f96a8b0d0efd46ab223dc0d360ea7a48302dea0b /vernac/vernacentries.ml | |
| parent | 0a0e956929e28fd6f1c43f39d7b92aeeaf0f01e2 (diff) | |
[vernac] use plain strings as attribute names
The concrete syntax is still restricted to identifiers.
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 5 |
1 files changed, 2 insertions, 3 deletions
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 |