aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/printmod.ml
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2013-10-28 14:08:46 +0100
committerGravatar Matthieu Sozeau <mattam@mattam.org>2014-05-06 09:58:54 +0200
commit001ff72b2c17fb7b2fcaefa2555c115f0d909a03 (patch)
tree9e83ae395173699a7c5b6f00648c4336bedb7afd /printing/printmod.ml
parent84cbc09bd1400f732a6c70e8a840e4c13d018478 (diff)
Initial work on reintroducing old-style polymorphism for compatibility (the stdlib does not compile entirely).
Diffstat (limited to 'printing/printmod.ml')
-rw-r--r--printing/printmod.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml
index da5546bac..8d05e2d6d 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -146,7 +146,8 @@ let print_body is_impl env mp (l,body) =
| None -> mt ()
| Some env ->
str " :" ++ spc () ++
- hov 0 (Printer.pr_ltype_env env cb.const_type) ++
+ hov 0 (Printer.pr_ltype_env env
+ (Typeops.type_of_constant_type env cb.const_type)) ++
(match cb.const_body with
| Def l when is_impl ->
spc () ++