diff options
| author | Hugo Herbelin | 2016-04-17 22:21:54 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-19 09:43:40 +0200 |
| commit | 7f85eb4f4cba0194f68034d6ccc0de0be9b5f067 (patch) | |
| tree | f557903ae68a145da6d1c2416f5e520cb9aa5c89 /dev/base_include | |
| parent | d926105c022177b70578982d037b12e5d914922b (diff) | |
Revert "Fixing printing of surrounding parentheses in "ltac:"."
I made a confusion between ltac: in constr and ltac: in tactics, the
one needing parentheses in v8.5 but the latter needing parentheses
only in trunk.
This reverts commit f5dc54519f2a62bab2f7b9059e8c3c8dc53619be.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions