diff options
author | 2016-11-05 11:33:42 +0100 | |
---|---|---|
committer | 2016-11-05 11:33:42 +0100 | |
commit | 29ff821da57e35d37b41be34febb275306c4809f (patch) | |
tree | 9cab0a1e063318ad2d53e4f755a728a41262307f /ltac | |
parent | f558a0552b49b533c1c79ee3eb6d49015eeb6084 (diff) |
Minor fix in documentation
Diffstat (limited to 'ltac')
0 files changed, 0 insertions, 0 deletions