Vecnacentries.dump_global silently ignores exceptions

So PrintName and Extraction dump globals when they exist

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15691 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 6 insertions, 3 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a4a14b7b3..7a786ce92 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -421,9 +421,10 @@ let smart_global r =
     gr
 
 let dump_global r =
-  let gr = Smartlocate.smart_global r in
+  try
+    let gr = Smartlocate.smart_global r in
     Dumpglob.add_glob (Genarg.loc_of_or_by_notation loc_of_reference r) gr
-
+  with _ -> ()
 (**********)
 (* Syntax *)
 
@@ -1347,7 +1348,7 @@ let vernac_print = function
   | PrintNamespace ns -> print_namespace ns
   | PrintMLLoadPath -> msg_notice (Mltop.print_ml_path ())
   | PrintMLModules -> msg_notice (Mltop.print_ml_modules ())
-  | PrintName qid -> msg_notice (print_name qid)
+  | PrintName qid -> dump_global qid; msg_notice (print_name qid)
   | PrintGraph -> msg_notice (Prettyp.print_graph())
   | PrintClasses -> msg_notice (Prettyp.print_classes())
   | PrintTypeClasses -> msg_notice (Prettyp.print_typeclasses())
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index dbceaaaa1..b49c01f89 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -13,6 +13,8 @@ open Vernacexpr
 open Constrexpr
 open Misctypes
 
+val dump_global : Libnames.reference or_by_notation -> unit
+
 (** Vernacular entries *)
 
 val show_script : unit -> unit