diff options
| author | Hugo Herbelin | 2017-11-24 19:00:13 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-11-24 19:00:13 +0100 |
| commit | 2bd31e5fffbd6722f20016c3962088ab2008e2c0 (patch) | |
| tree | 46f4b5a2d01cbaf88a3c1842bd78b056d1d385a2 /dev | |
| parent | d0305718b4141aa08675743d4f85238301f37ad7 (diff) | |
A possible fix after PR#6158 (raw/glob generic printers for ltac values).
Can the printers exploit the ability to now take an environment?
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions