Fixing printing in debugger (no global env in debugger).

1 files changed, 9 insertions, 1 deletions

diff --git a/engine/namegen.ml b/engine/namegen.ml
index bc04e3e48..84eb98684 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -191,18 +191,26 @@ let visible_ids (nenv, c) =
     let (gseen, vseen, ids) = !accu in
     let g = global_of_constr c in
     if not (Refset_env.mem g gseen) then
+      begin
+      try
       let gseen = Refset_env.add g gseen in
       let short = shortest_qualid_of_global Id.Set.empty g in
       let dir, id = repr_qualid short in
       let ids = if DirPath.is_empty dir then Id.Set.add id ids else ids in
       accu := (gseen, vseen, ids)
+      with Not_found when !Flags.in_debugger || !Flags.in_toplevel -> ()
+      end
   | Rel p ->
     let (gseen, vseen, ids) = !accu in
     if p > n && not (Int.Set.mem p vseen) then
       let vseen = Int.Set.add p vseen in
       let name =
         try Some (lookup_name_of_rel (p - n) nenv)
-        with Not_found -> None (* Unbound indice : may happen in debug *)
+        with Not_found ->
+          (* Unbound index: may happen in debug and actually also
+             while computing temporary implicit arguments of an
+             inductive type *)
+          None
       in
       let ids = match name with
       | Some (Name id) -> Id.Set.add id ids