aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/ppvernac.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/ppvernac.ml')
-rw-r--r--parsing/ppvernac.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index c2571ad0a..9b0186368 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -484,7 +484,7 @@ let rec pr_vernac = function
| None -> mt()
| Some r ->
str"Eval" ++ spc() ++
- pr_red_expr (pr_constr, pr_lconstr, pr_reference) r ++
+ pr_red_expr (pr_constr, pr_lconstr, pr_or_by_notation pr_reference) r ++
str" in" ++ spc() in
let pr_def_body = function
| DefineBody (bl,red,body,d) ->
@@ -776,7 +776,7 @@ let rec pr_vernac = function
let pr_mayeval r c = match r with
| Some r0 ->
hov 2 (str"Eval" ++ spc() ++
- pr_red_expr (pr_constr,pr_lconstr,pr_reference) r0 ++
+ pr_red_expr (pr_constr,pr_lconstr,pr_or_by_notation pr_reference) r0 ++
spc() ++ str"in" ++ spc () ++ pr_constr c)
| None -> hov 2 (str"Check" ++ spc() ++ pr_constr c)
in