diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 13 |
1 files changed, 3 insertions, 10 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index d9410a0885..dc418d530e 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -29,17 +29,10 @@ open Printer module Tag = struct - let keyword = - let style = Terminal.make ~bold:true () in - Ppstyle.make ~style ["tactic"; "keyword"] - let primitive = - let style = Terminal.make ~fg_color:`LIGHT_GREEN () in - Ppstyle.make ~style ["tactic"; "primitive"] - - let string = - let style = Terminal.make ~fg_color:`LIGHT_RED () in - Ppstyle.make ~style ["tactic"; "string"] + let keyword = "tactic.keyword" + let primitive = "tactic.primitive" + let string = "tactic.string" end |