diff options
| author | Théo Zimmermann | 2019-06-14 18:10:20 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-06-15 12:54:35 +0200 |
| commit | c4ceebf9967b2387e7092b52bffd68cbbb3707e6 (patch) | |
| tree | a6c71ed6acb08f58f53b52f47f579c0c3e669d84 /doc/plugin_tutorial | |
| parent | a024cf9c61b57860ce3e679be4fae427996320db (diff) | |
Rename expr and tacexpr tokens into ltac_expr token family.
This allows to refer to them from other part of the manual without any ambiguity.
Diffstat (limited to 'doc/plugin_tutorial')
0 files changed, 0 insertions, 0 deletions