- Cleaning phase of the interfaces of libnames.ml and nametab.ml

  (uniformisation of function names, classification). One of the most
  visible change is the renaming of section_path into full_path (the
  use of name section was obsolete due to the module system, but I
  don't know if the new name is the best chosen one - especially it 
  remains some "sp" here and there).
- Simplification of the interface of classify_object (first argument dropped).
- Simplification of the code for vernac keyword "End".
- Other small cleaning or dead code removal.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12265 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 18 deletions

diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index cf88256bc..538828fca 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -191,7 +191,7 @@ let locate_any_name ref =
   let (loc,qid) = qualid_of_reference ref in
   try Term (N.locate qid)
   with Not_found -> 
-  try Syntactic (N.locate_syntactic_definition qid)
+  try Syntactic (N.locate_syndef qid)
   with Not_found ->
   try Dir (N.locate_dir qid)
   with Not_found ->
@@ -205,9 +205,9 @@ let pr_located_qualid = function
 	| IndRef _ -> "Inductive"
 	| ConstructRef _ -> "Constructor"
 	| VarRef _ -> "Variable" in
-      str ref_str ++ spc () ++ pr_sp (Nametab.sp_of_global ref)
+      str ref_str ++ spc () ++ pr_global ref
   | Syntactic kn ->
-      str "Notation" ++ spc () ++ pr_sp (Nametab.sp_of_syntactic_definition kn)
+      str "Notation" ++ spc () ++ pr_path (Nametab.path_of_syndef kn)
   | Dir dir ->
       let s,dir = match dir with
 	| DirOpenModule (dir,_) -> "Open Module", dir
@@ -218,7 +218,7 @@ let pr_located_qualid = function
       in
       str s ++ spc () ++ pr_dirpath dir
   | ModuleType (qid,_) ->
-      str "Module Type" ++ spc () ++ pr_sp (Nametab.full_name_modtype qid)
+      str "Module Type" ++ spc () ++ pr_path (Nametab.full_name_modtype qid)
   | Undefined qid ->    
       pr_qualid qid ++ spc () ++ str "not a defined object."
 
@@ -228,9 +228,9 @@ let print_located_qualid ref =
   let expand = function
     | TrueGlobal ref ->
 	Term ref, N.shortest_qualid_of_global Idset.empty ref
-    | SyntacticDef kn ->
+    | SynDef kn ->
 	Syntactic kn, N.shortest_qualid_of_syndef Idset.empty kn in
-  match List.map expand (N.extended_locate_all qid) with
+  match List.map expand (N.locate_extended_all qid) with
     | [] -> 
 	let (dir,id) = repr_qualid qid in
 	if dir = empty_dirpath then
@@ -636,18 +636,6 @@ let print_name ref =
     let (_,c,typ) = Global.lookup_named str in 
     (print_named_decl (str,c,typ))
   with Not_found ->
-  try 
-    let sp = Nametab.locate_obj qid in
-    let (oname,lobj) = 
-      let (oname,entry) =
-	List.find (fun en -> (fst (fst en)) = sp) (Lib.contents_after None)
-      in
-      match entry with
-	| Lib.Leaf obj -> (oname,obj)
-	| _ -> raise Not_found
-    in
-    print_leaf_entry true (oname,lobj)
-  with Not_found ->
     errorlabstrm
       "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")