aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/printmod.ml
diff options
context:
space:
mode:
Diffstat (limited to 'printing/printmod.ml')
-rw-r--r--printing/printmod.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 5c7dcdc10..219eafda4 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -323,7 +323,7 @@ let print_body is_impl env mp (l,body) =
str " :" ++ spc () ++
hov 0 (Printer.pr_ltype_env env sigma
(Vars.subst_instance_constr u
- (Typeops.type_of_constant_type env cb.const_type))) ++
+ cb.const_type)) ++
(match cb.const_body with
| Def l when is_impl ->
spc () ++