diff options
| author | Hugo Herbelin | 2014-10-01 20:04:01 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-01 20:19:26 +0200 |
| commit | 3741c46fe134ca42a8f056258a21668fa0e0c551 (patch) | |
| tree | 324180a46057b02d55528b9779435b6a8b30fc01 /lib/cArray.ml | |
| parent | d1c71b1f3b11e2eb29a5898610d6128b7d535337 (diff) | |
Fixing nice printing of error reporting with ml tactics bound to ltac names.
Diffstat (limited to 'lib/cArray.ml')
0 files changed, 0 insertions, 0 deletions