diff options
| author |  coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-08-13 14:44:24 +0000 |
|---|---|---|
| committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-08-13 14:44:24 +0000 |
| commit | a3848b0a10064fb7e206a503ac8b829cb9ce4666 (patch) | |
| tree | 57715eb46564f71b91825c46ecb432a41c1ec095 /toplevel | |
| parent | bc4e7b8c2317b2536eb42efb7cbf37d748ceb7c6 (diff) | |
Petites corrections ici et la
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2961 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 16 |
1 files changed, 15 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 6e0ba7087..f3e2ac0f1 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -205,6 +205,20 @@ let print_located_qualid (_,qid) = let sp = Nametab.sp_of_syntactic_definition kn in msgnl (pr_sp sp) with Not_found -> + try + let dir = match Nametab.locate_dir qid with + | DirOpenModule (dir,_) + | DirOpenModtype (dir,_) + | DirOpenSection (dir,_) + | DirModule (dir,_) + | DirClosedSection dir -> dir + in + msgnl (pr_dirpath dir) + with Not_found -> + try + let (_,sp) = Nametab.full_name_modtype qid in + msgnl (pr_sp sp) + with Not_found -> msgnl (pr_qualid qid ++ str " is not a defined object") (*let print_path_entry (s,l) = @@ -426,7 +440,7 @@ let vernac_declare_module_type id bl mty_ast_o = | _, None -> Declaremods.start_modtype id argids args; if_verbose message - ("Interactive Module "^ string_of_id id ^" started") + ("Interactive Module Type "^ string_of_id id ^" started") | _, Some base_mty -> let mty = |