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/vernacexpr.ml | |
| parent | 0a0e956929e28fd6f1c43f39d7b92aeeaf0f01e2 (diff) | |
[vernac] use plain strings as attribute names
The concrete syntax is still restricted to identifiers.
Diffstat (limited to 'vernac/vernacexpr.ml')
| -rw-r--r-- | vernac/vernacexpr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 2287630c7..e97cac818 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -459,7 +459,7 @@ type nonrec vernac_expr = (* For extension *) | VernacExtend of extend_name * Genarg.raw_generic_argument list -type vernac_flags = (Names.Id.t * vernac_flag_value) list +type vernac_flags = (string * vernac_flag_value) list and vernac_flag_value = | VernacFlagEmpty | VernacFlagLeaf of string |