aboutsummaryrefslogtreecommitdiff
path: root/printing/printmod.ml
diff options
context:
space:
mode:
Diffstat (limited to 'printing/printmod.ml')
-rw-r--r--printing/printmod.ml3
1 files changed, 1 insertions, 2 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 112abeec9c..da5546baca 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -146,8 +146,7 @@ let print_body is_impl env mp (l,body) =
| None -> mt ()
| Some env ->
str " :" ++ spc () ++
- hov 0 (Printer.pr_ltype_env env
- (Typeops.type_of_constant_type env cb.const_type)) ++
+ hov 0 (Printer.pr_ltype_env env cb.const_type) ++
(match cb.const_body with
| Def l when is_impl ->
spc () ++