diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-12 17:18:36 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:04 +0100 |
| commit | 6901f720c6115c8eec1343846641a5c8453c3268 (patch) | |
| tree | 9b70fb5c3c251df46d8d960e2ae6ba634b5faf96 /vernac/metasyntax.ml | |
| parent | 00c3248a80253eb28a3779e8640101d8c83ab5d2 (diff) | |
Notations: documenting structure collecting variables occurring in notation.
Diffstat (limited to 'vernac/metasyntax.ml')
0 files changed, 0 insertions, 0 deletions