diff options
| -rw-r--r-- | printing/pptactic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |