diff options
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppvernacnew.ml | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index 00351a919..6ec54c8f1 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -545,14 +545,17 @@ let rec pr_vernac = function let pr_constructor_list l = match l with | [] -> mt() | _ -> - fnl() ++ str" | " ++ + fnl() ++ str (if List.length l = 1 then " " else " | ") ++ prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l in - let pr_oneind (id,indpar,s,lc) = - hov 0 (pr_id id ++ spc() ++ pr_sbinders indpar ++ str":" ++ spc() ++ - pr_lconstr s ++ str" :=") ++ pr_constructor_list lc in + let pr_oneind key (id,indpar,s,lc) = + hov 0 (str key ++ spc() ++ pr_id id ++ spc() ++ + pr_sbinders indpar ++ str":" ++ spc() ++ + pr_lconstr s ++ str" :=") ++ pr_constructor_list lc in hov 1 - ((if f then str"Inductive" else str"CoInductive") ++ spc() ++ - prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_oneind l) + (pr_oneind (if f then "Inductive" else "CoInductive") (List.hd l)) ++ + hov 1 + (prlist (fun ind -> fnl() ++ pr_oneind "with" ind) + (List.tl l)) | VernacFixpoint recs -> |