Affichage des inductifs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3896 85f007b7-540e-0410-9357-904b9bb8a0f7

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 ->