diff options
| author | Pierre-Marie Pédrot | 2014-05-16 16:41:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-05-16 16:41:29 +0200 |
| commit | c2f78ed4fba9fa027fdf2051f214e1c5b4fe670e (patch) | |
| tree | 42f41ae796eb1051bc9735f4f3dd95b51a192091 | |
| parent | 7491ffa371ab7537dd4d7b85af1079a792dd6e96 (diff) | |
Slightly better printer for native ML tactics, in order to disambiguate
them.
| -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 |