aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/ppconstr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/ppconstr.ml')
-rw-r--r--parsing/ppconstr.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index fa0755364..16820efdc 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -629,7 +629,7 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) = function
| Red true -> error "Shouldn't be accessible from user."
| ExtraRedExpr s -> str s
- | CbvVm -> str "vm_compute"
+ | CbvVm o -> str "vm_compute" ++ pr_opt (pr_with_occurrences pr_pattern) o
let rec pr_may_eval test prc prlc pr2 pr3 = function
| ConstrEval (r,c) ->