diff options
author | 2018-06-25 16:09:11 +0000 | |
---|---|---|
committer | 2018-07-03 16:10:16 +0000 | |
commit | d3127693d4a2125088aa512f593d782843482f2a (patch) | |
tree | f96a8b0d0efd46ab223dc0d360ea7a48302dea0b /kernel/esubst.mli | |
parent | 0a0e956929e28fd6f1c43f39d7b92aeeaf0f01e2 (diff) |
[vernac] use plain strings as attribute names
The concrete syntax is still restricted to identifiers.
Diffstat (limited to 'kernel/esubst.mli')
0 files changed, 0 insertions, 0 deletions