From 3741c46fe134ca42a8f056258a21668fa0e0c551 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 1 Oct 2014 20:04:01 +0200
Subject: Fixing nice printing of error reporting with ml tactics bound to ltac
 names.

---
 dev/printers.mllib | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'dev')

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
-- 
cgit v1.2.3