diff options
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index fca33a24bf..f55bfb504f 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -304,6 +304,12 @@ let print_inductive_argument_scopes = print_args_data_of_inductive_ids Notation.find_arguments_scope (Option.has_some) print_argument_scopes +let print_bidi_hints gr = + match Pretyping.get_bidirectionality_hint gr with + | None -> [] + | Some nargs -> + [str "Using typing information from context after typing the " ++ int nargs ++ str " first arguments"] + (*********************) (* "Locate" commands *) @@ -841,7 +847,8 @@ let print_about_any ?loc env sigma k udecl = print_name_infos ref @ (if Pp.ismt rb then [] else [rb]) @ print_opacity ref @ - [hov 0 (str "Expands to: " ++ pr_located_qualid k)]) + print_bidi_hints ref @ + [hov 0 (str "Expands to: " ++ pr_located_qualid k)]) | Syntactic kn -> let () = match Syntax_def.search_syntactic_definition kn with | [],Notation_term.NRef ref -> Dumpglob.add_glob ?loc ref |