diff options
Diffstat (limited to 'parsing/prettyp.ml')
| -rw-r--r-- | parsing/prettyp.ml | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index e30979bf..d3eb40d0 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -673,16 +673,20 @@ let print_opaque_name qid = let (_,c,ty) = lookup_named id env in print_named_decl (id,c,ty) -let print_about_any k = +let print_about_any loc k = match k with | Term ref -> + Dumpglob.add_glob loc ref; pr_infos_list - ([print_ref false ref; blankline] @ + (print_ref false ref :: blankline :: print_name_infos ref @ print_simpl_behaviour ref @ print_opacity ref @ [hov 0 (str "Expands to: " ++ pr_located_qualid k)]) | Syntactic kn -> + let () = match Syntax_def.search_syntactic_definition kn with + | [],Topconstr.ARef ref -> Dumpglob.add_glob loc ref + | _ -> () in v 0 ( print_syntactic_def kn ++ hov 0 (str "Expands to: " ++ pr_located_qualid k)) ++ fnl() @@ -691,11 +695,11 @@ let print_about_any k = let print_about = function | Genarg.ByNotation (loc,ntn,sc) -> - print_about_any + print_about_any loc (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true) ntn sc)) | Genarg.AN ref -> - print_about_any (locate_any_name ref) + print_about_any (loc_of_reference ref) (locate_any_name ref) (* for debug *) let inspect depth = |