diff options
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 24b0dc6cd..b78e73e48 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -260,7 +260,7 @@ let pr_module_vardecls pr_c (export,idl,(mty,inl)) = let lib_dir = Lib.library_dp() in List.iter (fun (_,id) -> Declaremods.process_module_bindings [id] - [make_mbid lib_dir id, + [MBId.make lib_dir id, (Modintern.interp_modtype (Global.env()) mty, inl)]) idl; (* Builds the stream *) spc() ++ |