summaryrefslogtreecommitdiff
path: root/src/pretty_print_common.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/pretty_print_common.ml')
-rw-r--r--src/pretty_print_common.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml
index 57a06e74..bd43c1a7 100644
--- a/src/pretty_print_common.ml
+++ b/src/pretty_print_common.ml
@@ -46,6 +46,7 @@ open PPrint
let pipe = string "|"
let arrow = string "->"
let dotdot = string ".."
+let coloncolon = string "::"
let coloneq = string ":="
let lsquarebar = string "[|"
let rsquarebar = string "|]"