diff options
| author | Clément Pit-Claudel | 2019-06-15 09:16:16 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2019-06-15 09:16:16 -0400 |
| commit | a286c524a57597e6e29f17cdfa8c4af82cbb494c (patch) | |
| tree | 795ca672832a802b958edf657da9d2e9fb5d15fb /doc/plugin_tutorial | |
| parent | 689cfd0674fd79a21008fa7efe17774d5efaf30f (diff) | |
| parent | c4ceebf9967b2387e7092b52bffd68cbbb3707e6 (diff) | |
Merge PR #10377: Rename expr and tacexpr tokens into ltac_expr token family.
Reviewed-by: cpitclaudel
Diffstat (limited to 'doc/plugin_tutorial')
0 files changed, 0 insertions, 0 deletions