aboutsummaryrefslogtreecommitdiff
path: root/printing/prettyp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'printing/prettyp.ml')
-rw-r--r--printing/prettyp.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 8b835310de..1810cc6588 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -902,7 +902,7 @@ let inspect env sigma depth =
open Classops
-let print_coercion_value env sigma v = pr_lconstr_env env sigma (get_coercion_value v)
+let print_coercion_value env sigma v = Printer.pr_global v.coe_value
let print_class i =
let cl,_ = class_info_from_index i in