aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/ppconstr.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 6d34b10bc..e7f4a0b24 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -624,6 +624,8 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) = function
hov 1 (str "cbv" ++ pr_red_flag pr_ref f)
| Lazy f ->
hov 1 (str "lazy" ++ pr_red_flag pr_ref f)
+ | Cbn f ->
+ hov 1 (str "cbn" ++ pr_red_flag pr_ref f)
| Unfold l ->
hov 1 (str "unfold" ++ spc() ++
prlist_with_sep pr_comma (pr_with_occurrences pr_ref) l)