diff options
Diffstat (limited to 'parsing/ppconstr.ml')
| -rw-r--r-- | parsing/ppconstr.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 3a02e5f25..3bfd26d72 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -372,6 +372,8 @@ let pr_red_expr (pr_constr,pr_ref) = function | Red true -> error "Shouldn't be accessible from user" | ExtraRedExpr (s,c) -> hov 1 (str s ++ pr_arg pr_constr c) + | CbvVm -> str "vm_compute" + let rec pr_may_eval pr pr2 = function | ConstrEval (r,c) -> |