From c2f78ed4fba9fa027fdf2051f214e1c5b4fe670e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 16 May 2014 16:41:29 +0200
Subject: Slightly better printer for native ML tactics, in order to
 disambiguate them.

---
 printing/pptactic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index e74dd9fc15..ffb0d7a369 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -264,7 +264,7 @@ let pr_extend_gen pr_gen lev s l =
     let p = pr_tacarg_using_rule pr_gen (pl,l) in
     if lev' > lev then surround p else p
   with Not_found ->
-    str s ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)"
+    str "<" ++ str s ++ str ">" ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)"
 
 let pr_alias_gen pr_gen lev key l =
   try
-- 
cgit v1.2.3