diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-03-27 23:17:50 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-03-27 23:22:05 +0200 |
| commit | 27ce382bcfefafa5efae3bc734e8c4c235fe0261 (patch) | |
| tree | 8a2ca4a40ea77fe1474396e8b31e64146827bf2d /printing | |
| parent | 7535e268f7706d1dee263fdbafadf920349103db (diff) | |
Do so that "About" tells if a reference is a coercion.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/prettyp.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 8fabb7053..5963d45ef 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -204,6 +204,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 = @@ -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 |