diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-07-27 13:54:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-07-27 13:54:25 +0200 |
| commit | cf193df65c53813054239463f6496526533e9bab (patch) | |
| tree | f2d9c248a3ee838ae7140c831422e2faad218528 /printing/printmod.ml | |
| parent | 20147a19e9f9a2bbeab5612c7ac17baaaf810af5 (diff) | |
Fixing bug #2169:
"Print Module command shows module type expression incorrectly".
Diffstat (limited to 'printing/printmod.ml')
| -rw-r--r-- | printing/printmod.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml index 295d8aaa6..a80bbb146 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -315,15 +315,17 @@ let rec print_typ_expr env mp locals mty = let mapp = List.tl lapp in hov 3 (str"(" ++ (print_kn locals fapp) ++ spc () ++ prlist_with_sep spc (print_modpath locals) mapp ++ str")") - | MEwith(me,WithDef(idl,c))-> + | MEwith(me,WithDef(idl,(c, _)))-> let env' = None in (* TODO: build a proper environment if env <> None *) let s = String.concat "." (List.map Id.to_string idl) in hov 2 (print_typ_expr env' mp locals me ++ spc() ++ str "with" ++ spc() - ++ def "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc()) - | MEwith(me,WithMod(idl,mp))-> + ++ def "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc() + ++ Printer.pr_lconstr c) + | MEwith(me,WithMod(idl,mp'))-> let s = String.concat "." (List.map Id.to_string idl) in hov 2 (print_typ_expr env mp locals me ++ spc() ++ str "with" ++ spc() ++ - keyword "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc()) + keyword "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc() + ++ print_modpath locals mp') let print_mod_expr env mp locals = function | MEident mp -> print_modpath locals mp |