From 8af2350260ed17968557d7d723da5d8bf41bb5b2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 23 Oct 2003 19:16:34 +0000
Subject: Saut de ligne avant les infos non logiques de print_about

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4714 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/prettyp.ml | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 3cc8cea3af..ff6411a402 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -74,8 +74,10 @@ let print_argument_scopes = function
   | _  -> mt()
 
 let print_name_infos ref =
-  print_impl_args (implicits_of_global ref) ++
-  print_argument_scopes (Symbols.find_arguments_scope ref)
+  let impl = implicits_of_global ref in
+  let scopes = Symbols.find_arguments_scope ref in
+  (if impl<>[] or not (List.for_all ((=) None) scopes) then fnl() else mt())
+  ++ print_impl_args impl ++ print_argument_scopes scopes
 
 let print_id_args_data test pr id l =
   if List.exists test l then
@@ -469,14 +471,14 @@ let print_about ref =
       print_constant false " : " sp
   | Term (IndRef ind as ref) ->
       let ty = Inductive.type_of_inductive env ind in
-      print_typed_value (mkInd ind, ty) ++ fnl () ++
+      print_typed_value (mkInd ind, ty) ++ 
       print_name_infos ref
   | Term (ConstructRef cstr as ref) ->
       let ty = Inductive.type_of_constructor env cstr in
-      print_typed_value (mkConstruct cstr, ty) ++ fnl () ++
+      print_typed_value (mkConstruct cstr, ty) ++ 
       print_name_infos ref
   | Term (VarRef sp as ref) ->
-      print_named_decl (get_variable sp) ++ fnl () ++
+      print_named_decl (get_variable sp) ++ 
       print_name_infos ref
   | Syntactic kn ->
       print_syntactic_def " = " kn
-- 
cgit v1.2.3