From 373091ffbab347d8b75831e17f3e4384018facd8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 10 Apr 2003 21:59:38 +0000
Subject: Affichage des inductifs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3913 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 translate/ppvernacnew.ml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 6ec54c8f16..aa264293bf 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -551,11 +551,9 @@ let rec pr_vernac = function
 	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
-        (pr_oneind (if f then "Inductive" else "CoInductive") (List.hd l)) ++ 
-      hov 1
- 	(prlist (fun ind -> fnl() ++ pr_oneind "with" ind)
-	  (List.tl l))
+      hov 1 (pr_oneind (if f then "Inductive" else "CoInductive") (List.hd l))
+      ++ 
+      (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
 
   | VernacFixpoint recs ->
 
-- 
cgit v1.2.3