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 /dev | |
| parent | d1c71b1f3b11e2eb29a5898610d6128b7d535337 (diff) | |
Fixing nice printing of error reporting with ml tactics bound to ltac names.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/printers.mllib | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index a655bc5266..703c446478 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -192,6 +192,8 @@ Pptactic Ppdecl_proof Egramml Egramcoq +Tacsubst +Tacenv Himsg Cerrors Locality |