aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--printing/printer.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/printer.ml b/printing/printer.ml
index 47cf2ac1f3..82dda09344 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -260,7 +260,7 @@ let pr_var_decl_skel pr_id env sigma (id,c,typ) =
| None -> (mt ())
| Some c ->
(* Force evaluation *)
- let pb = pr_lconstr_core true env sigma c in
+ let pb = pr_lconstr_env env sigma c in
let pb = if isCast c then surround pb else pb in
(str" := " ++ pb ++ cut () ) in
let pt = pr_ltype_env env sigma typ in
@@ -278,7 +278,7 @@ let pr_rel_decl env sigma (na,c,typ) =
| None -> mt ()
| Some c ->
(* Force evaluation *)
- let pb = pr_lconstr_core true env sigma c in
+ let pb = pr_lconstr_env env sigma c in
let pb = if isCast c then surround pb else pb in
(str":=" ++ spc () ++ pb ++ spc ()) in
let ptyp = pr_ltype_env env sigma typ in