diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-21 15:27:07 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-21 15:27:07 +0000 |
| commit | b0098b7e2f0120941a3f8201788e167727476e51 (patch) | |
| tree | f6840cee75eadcba6a4e02540224d9be7e6dfa6e /parsing/printmod.ml | |
| parent | 7da3e3d85c88eb42e932230048cb0db255474b5d (diff) | |
Restore display of notation when printing an inductive such as sig
+ minor pp improvement for Print Module Type
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14148 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/printmod.ml')
| -rw-r--r-- | parsing/printmod.ml | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/parsing/printmod.ml b/parsing/printmod.ml index f258da587..cf2aad203 100644 --- a/parsing/printmod.ml +++ b/parsing/printmod.ml @@ -124,7 +124,7 @@ let print_body is_impl env mp (l,body) = | SFBmind mib -> try let env = Option.get env in - Printer.pr_mutual_inductive_body env mib + Printer.pr_mutual_inductive_body env (make_mind mp empty_dirpath l) mib with _ -> (if mib.mind_finite then str "Inductive " else str "CoInductive") ++ name) @@ -248,9 +248,10 @@ let print_module with_body mp = let print_modtype kn = let mtb = Global.lookup_modtype kn in let name = print_kn [] kn in - str "Module Type " ++ name ++ str " = " ++ - (try - if !short then raise ShortPrinting; - print_modtype' (Some (Global.env ())) kn mtb.typ_expr - with _ -> - print_modtype' None kn mtb.typ_expr) + hv 1 + (str "Module Type " ++ name ++ str " =" ++ spc () ++ + (try + if !short then raise ShortPrinting; + print_modtype' (Some (Global.env ())) kn mtb.typ_expr + with _ -> + print_modtype' None kn mtb.typ_expr)) |