diff options
| author | herbelin | 2003-10-23 19:16:34 +0000 |
|---|---|---|
| committer | herbelin | 2003-10-23 19:16:34 +0000 |
| commit | 8af2350260ed17968557d7d723da5d8bf41bb5b2 (patch) | |
| tree | 56a64b7061b5c2fd5bcc5eb6379a7b1fcaf193b3 | |
| parent | 64921b7e96c081f1d9d39ffe636bd34bc0129200 (diff) | |
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
| -rw-r--r-- | parsing/prettyp.ml | 12 |
1 files 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 |