diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index de728ee15e..9b626d8bcf 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -121,16 +121,13 @@ let locate_file f = let print_located_qualid qid = try - let ref = Nametab.locate qid in - mSG - [< pr_id (Termops.id_of_global (Global.env()) ref); 'fNL >] + let sp = Nametab.sp_of_global (Global.env()) (Nametab.locate qid) in + mSG [< pr_sp sp; 'fNL >] with Not_found -> try - mSG - [< 'sTR (string_of_path (Syntax_def.locate_syntactic_definition qid)); - 'fNL >] + mSG [< pr_sp (Syntax_def.locate_syntactic_definition qid); 'fNL >] with Not_found -> - error ((Nametab.string_of_qualid qid) ^ " not a defined object") + error ((Nametab.string_of_qualid qid) ^ " is not a defined object") let print_path_entry (s,l) = [< 'sTR s; 'tBRK (0,2); 'sTR (string_of_dirpath l) >] |