diff options
| author | Yann Régis-Gianas | 2014-11-05 08:45:40 +0100 |
|---|---|---|
| committer | Yann Régis-Gianas | 2014-11-05 14:31:41 +0100 |
| commit | b6d282b96e332643c1ff6ae63d19602f9b6f5a73 (patch) | |
| tree | c36c9615f6e624d1007b8e9e647ed0cb26422cf0 /kernel/type_errors.ml | |
| parent | 683bd2db32025b38ac0d9a884bd4a3965daf21f8 (diff) | |
printing/Ppvernac: Fix missing keyword tagging on definition introducers.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions