diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-01-14 23:34:52 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-01-16 13:33:03 +0100 |
| commit | 28ac569f0f8a0ae27552e4e4c20fc06ce12c720d (patch) | |
| tree | cde053a11fe0070e0a42065c79d1980bf5dd064a /.dir-locals.el | |
| parent | 448866f0ec5291d58677d8fccbefde493ade0ee2 (diff) | |
Tactic notation printing accesses all the token data.
Diffstat (limited to '.dir-locals.el')
0 files changed, 0 insertions, 0 deletions