aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/ppconstr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'printing/ppconstr.ml')
-rw-r--r--printing/ppconstr.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 8cfc3f9d9..c077fbe83 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -639,7 +639,7 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) = function
| ExtraRedExpr s -> str s
| CbvVm o -> str "vm_compute" ++ pr_opt (pr_with_occurrences pr_pattern) o
-let rec pr_may_eval test prc prlc pr2 pr3 = function
+let pr_may_eval test prc prlc pr2 pr3 = function
| ConstrEval (r,c) ->
hov 0
(str "eval" ++ brk (1,1) ++