diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-29 10:34:51 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-29 10:34:51 +0000 |
| commit | e9d2a45987b0b4fcfa7ec4d14e35e9a7a0d62028 (patch) | |
| tree | db8ec6dd826e103f725ac023eb7b3cca2357b0e1 /toplevel/vernacentries.ml | |
| parent | 86952ac8ad1dba395cb4724ac0b4f54774448944 (diff) | |
reparation de Locate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2247 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/vernacentries.ml')
| -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 de728ee15..9b626d8bc 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) >] |