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