aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/states.mli
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2016-01-20 15:57:24 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-01-20 15:57:24 +0100
commitaf5eafaee218935c35f0bd906727d2d2370bd136 (patch)
tree56b71394d5f39aab76b2351687d4a6df277abb7b /library/states.mli
parent1af878e0dac2198ae487d0b37438520772f28350 (diff)
Change $(...)$ to ltac:(...) in section 2.11. Fixes #4500.
Diffstat (limited to 'library/states.mli')
0 files changed, 0 insertions, 0 deletions