From f54192a50eaf14852e1462f24e4168aa8a8545fe Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 20 Jul 2018 18:01:18 +0200
Subject: Coercions cleanup: use GlobRef.t instead of constr

---
 printing/prettyp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing/prettyp.ml')

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 7258bb9b72..02968b9d67 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -909,7 +909,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
-- 
cgit v1.2.3