aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/printmod.ml
diff options
context:
space:
mode:
Diffstat (limited to 'printing/printmod.ml')
-rw-r--r--printing/printmod.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 8d05e2d6d..b7be2c0f5 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -153,8 +153,8 @@ let print_body is_impl env mp (l,body) =
spc () ++
hov 2 (str ":= " ++
Printer.pr_lconstr_env env (Mod_subst.force_constr l))
- | _ -> mt ()) ++
- str ".")
+ | _ -> mt ()) ++ str "." ++
+ Printer.pr_universe_ctx cb.const_universes)
| SFBmind mib ->
try
let env = Option.get env in