From 27ce382bcfefafa5efae3bc734e8c4c235fe0261 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 27 Mar 2017 23:17:50 +0200
Subject: Do so that "About" tells if a reference is a coercion.

---
 printing/prettyp.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 8fabb70536..5963d45ef9 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -203,6 +203,11 @@ let print_opacity ref =
           | TransparentMaybeOpacified Conv_oracle.Expand ->
               str "transparent (with minimal expansion weight)"]
 
+(*******************)
+
+let print_if_is_coercion ref =
+  if Classops.coercion_exists ref then [pr_global ref ++ str " is a coercion"] else []
+
 (*******************)
 (* *)
 
@@ -257,7 +262,8 @@ let print_name_infos ref =
   type_info_for_implicit @
   print_renames_list (mt()) renames @
   print_impargs_list (mt()) impls @
-  print_argument_scopes (mt()) scopes
+  print_argument_scopes (mt()) scopes @
+  print_if_is_coercion ref
 
 let print_id_args_data test pr id l =
   if List.exists test l then
-- 
cgit v1.2.3