diff options
| author | Hugo Herbelin | 2016-04-09 16:30:48 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-09 18:26:00 +0200 |
| commit | 41af4c3e36af15d9cc235cb5effedeed40478d2e (patch) | |
| tree | 899e0ca0e02752d6ff37228a7b5123305a47bff1 /kernel | |
| parent | fa2fa0b2e6ca0fbfb9a9278af211d4ef533b6791 (diff) | |
Re-add printer for tacdef_body so that Ltac definitions are printed by pr_vernac.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions