From 5cd253c4d8e046d7eac108b48be2d510c114a49a Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 6 Aug 2016 17:46:01 +0200 Subject: Fixing printing in debugger (no global env in debugger). --- engine/namegen.ml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'engine/namegen.ml') 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 -- cgit v1.2.3