diff options
| author | Maxime Dénès | 2016-01-20 15:57:24 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2016-01-20 15:57:24 +0100 |
| commit | af5eafaee218935c35f0bd906727d2d2370bd136 (patch) | |
| tree | 56b71394d5f39aab76b2351687d4a6df277abb7b /interp/stdarg.ml | |
| parent | 1af878e0dac2198ae487d0b37438520772f28350 (diff) | |
Change $(...)$ to ltac:(...) in section 2.11. Fixes #4500.
Diffstat (limited to 'interp/stdarg.ml')
0 files changed, 0 insertions, 0 deletions