aboutsummaryrefslogtreecommitdiff
path: root/printing/prettyp.ml
diff options
context:
space:
mode:
authorMaxime Dénès2017-04-04 16:55:56 +0200
committerMaxime Dénès2017-04-04 16:55:56 +0200
commitc112063ba5f562d511ed0cbd754a41539fc48fe1 (patch)
tree1f7e244b3d3b0963d07463604d77bdf35001e67c /printing/prettyp.ml
parentb824d8ad00001f6c41d0fc8bbf528dccb937c887 (diff)
parentea10a2da9ac11ea57e9eb80d0d6baf9321886da4 (diff)
Merge branch 'trunk' into pr379
Diffstat (limited to 'printing/prettyp.ml')
-rw-r--r--printing/prettyp.ml8
1 files changed, 7 insertions, 1 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 2fc8bc82d1..aa422e36af 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -205,6 +205,11 @@ let print_opacity ref =
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 []
+
+(*******************)
(* *)
let print_polymorphism ref =
@@ -258,7 +263,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