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/vernacinterp.ml | |
| parent | 0a0e956929e28fd6f1c43f39d7b92aeeaf0f01e2 (diff) | |
[vernac] use plain strings as attribute names
The concrete syntax is still restricted to identifiers.
Diffstat (limited to 'vernac/vernacinterp.ml')
0 files changed, 0 insertions, 0 deletions