- 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

4 files changed, 10 insertions, 22 deletions

diff --git a/plugins/interface/centaur.ml4 b/plugins/interface/centaur.ml4
index f8c088779..c8fc7bdf3 100644
--- a/plugins/interface/centaur.ml4
+++ b/plugins/interface/centaur.ml4
@@ -146,7 +146,7 @@ let ctf_acknowledge_command request_id command_count opt_exn =
         g_count, !current_goal_index
     else
       (0, 0)
-  and statnum = Lib.current_command_label ()
+  and statnum = Lib.current_state_label ()
   and dpth = let d = Pfedit.current_proof_depth() in if d >= 0 then d else 0
   and pending = CT_id_list (List.map xlate_ident (Pfedit.get_all_proof_names())) in
    (ctf_header "acknowledge" request_id ++
@@ -409,12 +409,12 @@ let inspect n =
 		  (match oname, object_tag lobj with
                        (sp,_), "VARIABLE" ->
 			 let (_, _, v) = Global.lookup_named (basename sp) in
-			   add_search2 (Nametab.locate (qualid_of_sp sp)) v
+			   add_search2 (Nametab.locate (qualid_of_path sp)) v
 		     | (sp,kn), "CONSTANT" ->
 			 let typ = Typeops.type_of_constant (Global.env()) (constant_of_kn kn) in
-			   add_search2 (Nametab.locate (qualid_of_sp sp)) typ
+			   add_search2 (Nametab.locate (qualid_of_path sp)) typ
 		     | (sp,kn), "MUTUALINDUCTIVE" ->
-			 add_search2 (Nametab.locate (qualid_of_sp sp))
+			 add_search2 (Nametab.locate (qualid_of_path sp))
 			   (Pretyping.Default.understand Evd.empty (Global.env())
 			      (RRef(dummy_loc, IndRef(kn,0))))
 		     | _ -> failwith ("unexpected value 1 for "^ 
@@ -764,12 +764,12 @@ let full_name_of_ref r =
      | ConstRef _ -> str "CST"
      | IndRef _ -> str "IND"
      | ConstructRef _ -> str "CSR")
-  ++ str " " ++ (pr_sp (Nametab.sp_of_global r))
+  ++ str " " ++ (pr_path (Nametab.path_of_global r))
     (* LEM TODO: Cleanly separate path from id (see Libnames.string_of_path) *)
 
 let string_of_ref =
   (*LEM TODO: Will I need the Var/Const/Ind/Construct info?*)
-  Depends.o Libnames.string_of_path Nametab.sp_of_global
+  Depends.o Libnames.string_of_path Nametab.path_of_global
 
 let print_depends compute_depends ptree =
   output_results (List.fold_left (fun x y -> x ++ (full_name_of_ref y) ++ fnl())
diff --git a/plugins/interface/coqparser.ml b/plugins/interface/coqparser.ml
index a63e18d27..df5e66b50 100644
--- a/plugins/interface/coqparser.ml
+++ b/plugins/interface/coqparser.ml
@@ -335,7 +335,7 @@ let print_version_action () =
 let load_syntax_action reqid module_name =
  msg (str "loading " ++ str module_name ++ str "... ");
  try
-      (let qid = Libnames.make_short_qualid (Names.id_of_string module_name) in
+      (let qid = Libnames.qualid_of_ident (Names.id_of_string module_name) in
       require_library [dummy_loc,qid] None;
       msg (str "opening... ");
       Declaremods.import_module false (Nametab.locate_module qid); 
diff --git a/plugins/interface/name_to_ast.ml b/plugins/interface/name_to_ast.ml
index 668a581e1..f5e8be31e 100644
--- a/plugins/interface/name_to_ast.ml
+++ b/plugins/interface/name_to_ast.ml
@@ -106,7 +106,7 @@ let convert_one_inductive sp tyi =
   let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp tyi in
   let env = Global.env () in
   let envpar = push_rel_context params env in
-  let sp = sp_of_global (IndRef (sp, tyi)) in
+  let sp = path_of_global (IndRef (sp, tyi)) in
   (((false,(dummy_loc,basename sp)),
    convert_env(List.rev params),
    Some (extern_constr true envpar arity), Vernacexpr.Inductive_kw ,
@@ -192,18 +192,6 @@ let leaf_entry_to_ast_list ((sp,kn),lobj) =
 let name_to_ast ref =
   let (loc,qid) = qualid_of_reference ref in
   let l = 
-    try
-      let sp = Nametab.locate_obj qid in
-      let (sp,lobj) = 
-      	let (sp,entry) =
-          List.find (fun en -> (fst (fst en)) = sp) (Lib.contents_after None)
-      	in
-	  match entry with
-            | Lib.Leaf obj -> (sp,obj)
-            | _ -> raise Not_found
-      in
-    	leaf_entry_to_ast_list (sp,lobj)
-    with Not_found -> 
       try 
     	match Nametab.locate qid with
 	  | ConstRef sp -> constant_to_ast_list sp
@@ -220,7 +208,7 @@ let name_to_ast ref =
 		   | Some c1 -> make_definition_ast name c1 typ [])
 	  with Not_found ->
 	    try
-	      let _sp = Nametab.locate_syntactic_definition qid in
+	      let _sp = Nametab.locate_syndef qid in
 		errorlabstrm "print"
       		  (str "printing of syntax definitions not implemented")
 	    with Not_found ->
diff --git a/plugins/interface/name_to_ast.mli b/plugins/interface/name_to_ast.mli
index f9e83b5e1..a532604f5 100644
--- a/plugins/interface/name_to_ast.mli
+++ b/plugins/interface/name_to_ast.mli
@@ -2,4 +2,4 @@ val name_to_ast : Libnames.reference -> Vernacexpr.vernac_expr;;
 val inductive_to_ast_list : Names.mutual_inductive -> Vernacexpr.vernac_expr list;;
 val constant_to_ast_list : Names.constant -> Vernacexpr.vernac_expr list;;
 val variable_to_ast_list : Names.variable -> Vernacexpr.vernac_expr list;;
-val leaf_entry_to_ast_list : (Libnames.section_path * Names.mutual_inductive) * Libobject.obj -> Vernacexpr.vernac_expr list;;
+val leaf_entry_to_ast_list : (Libnames.full_path * Names.mutual_inductive) * Libobject.obj -> Vernacexpr.vernac_expr list;;