diff options
| author | Hugo Herbelin | 2016-11-20 15:34:39 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2016-12-02 17:28:33 +0100 |
| commit | afab44873b7861d542cc0146d2bb8099d513f008 (patch) | |
| tree | bc4d35b9d263fd27f35d4fb012114f86978b9346 /dev/doc | |
| parent | ab3b0de5902082f7e692901979aa8330394c2f26 (diff) | |
Fixing printing of "ltac:" in tactics after surrounding parentheses
became mandatory.
Diffstat (limited to 'dev/doc')
0 files changed, 0 insertions, 0 deletions