diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-05 20:30:17 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-05 20:30:17 +0000 |
| commit | a353947b5c7645ccc6576bad0124ef6cca358001 (patch) | |
| tree | 11fd8e0a439c104322434cc08c0f12213b36014f /parsing | |
| parent | dd0fa1a38613af80e3b261eb5e6be1b6f40a8bda (diff) | |
Report 11364 de 8.2 vers trunk (bugs affichage Print Module)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11365 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/printmod.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/parsing/printmod.ml b/parsing/printmod.ml index 0bdae7c77..be73f573b 100644 --- a/parsing/printmod.ml +++ b/parsing/printmod.ml @@ -60,10 +60,10 @@ let rec print_module name locals with_body mb = in let modtype = match mb.mod_type with None -> str "" - | Some t -> str": " ++ + | Some t -> spc () ++ str": " ++ print_modtype locals t in - hv 2 (str "Module " ++ name ++ spc () ++ modtype ++ body) + hv 2 (str "Module " ++ name ++ modtype ++ body) and print_modtype locals mty = match mty with @@ -102,7 +102,7 @@ and print_sig locals msid sign = | SFBconst {const_opaque=true} -> str "Parameter " | SFBmind _ -> str "Inductive " | SFBmodule _ -> str "Module " - | SFBalias (mp,_) -> str "Module" + | SFBalias (mp,_) -> str "Module " | SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l) in prlist_with_sep spc print_spec sign @@ -114,7 +114,7 @@ and print_struct locals msid struc = | SFBconst {const_body=None} -> str "Parameter " | SFBmind _ -> str "Inductive " | SFBmodule _ -> str "Module " - | SFBalias (mp,_) -> str "Module" + | SFBalias (mp,_) -> str "Module " | SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l) in prlist_with_sep spc print_body struc @@ -125,9 +125,9 @@ and print_modexpr locals mexpr = match mexpr with (* let env' = Modops.add_module (MPbid mbid) (Modops.body_of_type mtb) env in *) let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals in - hov 2 (str "Functor" ++ spc() ++ str"[" ++ pr_id(id_of_mbid mbid) ++ + hov 2 (str "Functor" ++ spc() ++ str"(" ++ pr_id(id_of_mbid mbid) ++ str ":" ++ print_modtype locals mty.typ_expr ++ - str "]" ++ spc () ++ print_modexpr locals' mexpr) + str ")" ++ spc () ++ print_modexpr locals' mexpr) | SEBstruct (msid, struc) -> hv 2 (str "Struct" ++ spc () ++ print_struct locals msid struc ++ brk (1,-2) ++ str "End") | SEBapply (mexpr,marg,_) -> |