diff options
| author | Hugo Herbelin | 2017-11-04 23:16:26 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-11-04 23:17:23 +0100 |
| commit | 57f479f13c869408f51fbebc744c3b67a07d7f7c (patch) | |
| tree | 39137fb151bcd494c435e511343d3f6318c80363 /dev/include | |
| parent | 290e9585ac3b0f6ece3f1966457fef3811f88d10 (diff) | |
A possible fix after PR#6047 (a generic printer for ltac values).
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions