- 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

23 files changed, 63 insertions, 91 deletions

diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml
index 79ffaf3f9..3a408909d 100644
--- a/plugins/dp/dp.ml
+++ b/plugins/dp/dp.ml
@@ -115,7 +115,7 @@ let rename_global r =
 	s
       end
     in
-    loop (Nametab.id_of_global r)
+    loop (Nametab.basename_of_global r)
 
 let foralls =
   List.fold_right 
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 11c3b3b5b..e1edeec37 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -303,9 +303,9 @@ let ref_renaming_fun (k,r) =
     if l = [""] (* this happens only at toplevel of the monolithic case *)
     then
       let globs = Idset.elements (get_global_ids ()) in
-      let id = next_ident_away (kindcase_id k (safe_id_of_global r)) globs in
+      let id = next_ident_away (kindcase_id k (safe_basename_of_global r)) globs in
       string_of_id id
-    else modular_rename k (safe_id_of_global r)
+    else modular_rename k (safe_basename_of_global r)
   in
   add_global_ids (id_of_string s);
   s::l
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 39e277081..ba4786d37 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -506,7 +506,7 @@ let simple_extraction r = match locate_ref [r] with
 let extraction_library is_rec m =
   init true;
   let dir_m =
-    let q = make_short_qualid m in
+    let q = qualid_of_ident m in
     try Nametab.full_name_module q with Not_found -> error_unknown_module q
   in
   Visit.add_mp (MPfile dir_m);
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 83a780198..13a730ac2 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -182,7 +182,7 @@ let modular () = !modular_ref
    WARNING: for inductive objects, an extract_inductive must have been
    done before. *)
 
-let safe_id_of_global = function
+let safe_basename_of_global = function
   | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l
   | IndRef (kn,i) -> (snd (lookup_ind kn)).ind_packets.(i).ip_typename
   | ConstructRef ((kn,i),j) ->
@@ -191,7 +191,7 @@ let safe_id_of_global = function
 
 let safe_pr_global r =
  try Printer.pr_global r
- with _ -> pr_id (safe_id_of_global r)
+ with _ -> pr_id (safe_basename_of_global r)
 
 (* idem, but with qualification, and only for constants. *)
 
@@ -207,7 +207,7 @@ let pr_long_mp mp =
   let lid = repr_dirpath (Nametab.dir_of_mp mp) in
   str (String.concat "." (List.map string_of_id (List.rev lid)))
 
-let pr_long_global ref = pr_sp (Nametab.sp_of_global ref)
+let pr_long_global ref = pr_path (Nametab.path_of_global ref)
 
 (*S Warning and Error messages. *)
 
@@ -452,7 +452,7 @@ let (inline_extraction,_) =
        cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
        load_function = (fun _ (_,(b,l)) -> add_inline_entries b l);
        export_function = (fun x -> Some x);
-       classify_function = (fun (_,o) -> Substitute o);
+       classify_function = (fun o -> Substitute o);
        subst_function =
         (fun (_,s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
     }
@@ -535,7 +535,7 @@ let (blacklist_extraction,_) =
        cache_function = (fun (_,l) -> add_blacklist_entries l);
        load_function = (fun _ (_,l) -> add_blacklist_entries l);
        export_function = (fun x -> Some x);
-       classify_function = (fun (_,o) -> Libobject.Keep o);
+       classify_function = (fun o -> Libobject.Keep o);
        subst_function = (fun (_,_,x) -> x)
     }
 
@@ -595,7 +595,7 @@ let (in_customs,_) =
        cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s);
        load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s);
        export_function = (fun x -> Some x);
-       classify_function = (fun (_,o) -> Substitute o);
+       classify_function = (fun o -> Substitute o);
        subst_function =
         (fun (_,s,(r,ids,str)) -> (fst (subst_global s r), ids, str))
     }
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 6e3f2ec56..42ed6eef0 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -13,7 +13,7 @@ open Libnames
 open Miniml
 open Declarations
 
-val safe_id_of_global : global_reference -> identifier
+val safe_basename_of_global : global_reference -> identifier
 
 (*s Warning and Error messages. *)
 
diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4
index c9b993690..916294774 100644
--- a/plugins/field/field.ml4
+++ b/plugins/field/field.ml4
@@ -75,7 +75,7 @@ let (in_addfield,out_addfield)=
        Libobject.open_function = (fun i o -> if i=1 then cache_addfield o);
        Libobject.cache_function = cache_addfield;
        Libobject.subst_function = subst_addfield;
-       Libobject.classify_function = (fun (_,a) -> Libobject.Substitute a);
+       Libobject.classify_function = (fun a -> Libobject.Substitute a);
        Libobject.export_function = export_addfield }
 
 (* Adds a theory to the table *)
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index fc31ee6fc..75d69099a 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -45,7 +45,7 @@ let wrap n b continue seq gls=
     add_formula Concl dummy_id (pf_concl gls) seq1 gls else seq1 in
     continue seq2 gls
 
-let id_of_global=function
+let basename_of_global=function
     VarRef id->id
   | _->assert false
 
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index 1c2c93a49..b804c93ae 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -21,7 +21,7 @@ type 'a with_backtracking = tactic -> 'a
 
 val wrap : int -> bool -> seqtac
 
-val id_of_global: global_reference -> identifier
+val basename_of_global: global_reference -> identifier
 
 val clear_global: global_reference -> tactic
 
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index adfb9ce2f..9087f5179 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1000,7 +1000,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
 	      let finfos = find_Function_infos (destConst f) in 
 	      update_Function 
 		{finfos with
-		   equation_lemma = Some (match Nametab.locate (make_short_qualid equation_lemma_id) with
+		   equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with
 					      ConstRef c -> c
 					    | _ -> Util.anomaly "Not a constant" 
 					 )
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 348a17b11..46da3a01d 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -471,7 +471,7 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b
   in
   let ltof = 
     let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) in 
-    Libnames.Qualid (dummy_loc,Libnames.qualid_of_sp 
+    Libnames.Qualid (dummy_loc,Libnames.qualid_of_path 
       (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (id_of_string "ltof")))
   in
   let fun_from_mes = 
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index b29bdf3f1..868a876be 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -350,7 +350,7 @@ let subst_Function (_,subst,finfos) =
       is_general = finfos.is_general
     }
 
-let classify_Function (_,infos) = Libobject.Substitute infos
+let classify_Function infos = Libobject.Substitute infos
 
 let export_Function infos = Some infos
 
@@ -440,7 +440,7 @@ let _ =
 
 let find_or_none id = 
   try Some 
-    (match Nametab.locate (make_short_qualid id) with ConstRef c -> c | _ -> Util.anomaly "Not a constant" 
+    (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> Util.anomaly "Not a constant" 
     ) 
   with Not_found -> None
 
@@ -467,7 +467,7 @@ let add_Function is_general f =
   and rec_lemma = find_or_none (Nameops.add_suffix f_id "_rec")
   and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind")
   and graph_ind = 
-    match Nametab.locate (make_short_qualid (mk_rel_id f_id)) 
+    match Nametab.locate (qualid_of_ident (mk_rel_id f_id)) 
     with | IndRef ind -> ind | _ -> Util.anomaly "Not an inductive"
   in
   let finfos = 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 25e664336..876f3de4b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1386,7 +1386,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let tcc_lemma_constr = ref None in 
 (*   let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
   let hook _ _ =   
-    let term_ref = Nametab.locate (make_short_qualid term_id) in
+    let term_ref = Nametab.locate (qualid_of_ident term_id) in
     let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
 (*     message "start second proof"; *)
     let stop = ref false in 
@@ -1404,7 +1404,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
     end;
     if not !stop
     then
-      let eq_ref = Nametab.locate (make_short_qualid equation_id ) in
+      let eq_ref = Nametab.locate (qualid_of_ident equation_id ) in
       let f_ref = destConst (constr_of_global f_ref) 
       and functional_ref = destConst (constr_of_global functional_ref) 
       and eq_ref = destConst (constr_of_global eq_ref) in
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;;
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 8c8640ea5..075188f54 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -398,11 +398,11 @@ let destructurate_prop t =
     | _, [_;_] when c = Lazy.force coq_ge -> Kapp (Ge,args)
     | _, [_;_] when c = Lazy.force coq_gt -> Kapp (Gt,args)
     | Const sp, args ->
-	Kapp (Other (string_of_id (id_of_global (ConstRef sp))),args)
+	Kapp (Other (string_of_id (basename_of_global (ConstRef sp))),args)
     | Construct csp , args ->
-	Kapp (Other (string_of_id (id_of_global (ConstructRef csp))), args)
+	Kapp (Other (string_of_id (basename_of_global (ConstructRef csp))), args)
     | Ind isp, args ->
-	Kapp (Other (string_of_id (id_of_global (IndRef isp))),args)
+	Kapp (Other (string_of_id (basename_of_global (IndRef isp))),args)
     | Var id,[] -> Kvar id
     | Prod (Anonymous,typ,body), [] -> Kimp(typ,body)
     | Prod (Name _,_,_),[] -> error "Omega: Not a quantifier-free goal"
diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml
index 6dcc1e872..a07ec4757 100644
--- a/plugins/ring/ring.ml
+++ b/plugins/ring/ring.ml
@@ -274,7 +274,7 @@ let (theory_to_obj, obj_to_theory) =
 		    open_function = (fun i o -> if i=1 then cache_th o);
                     cache_function = cache_th;
 		    subst_function = subst_th;
-		    classify_function = (fun (_,x) -> Substitute x);
+		    classify_function = (fun x -> Substitute x);
 		    export_function = export_th }
 
 (* from the set A, guess the associated theory *)
@@ -733,7 +733,7 @@ let build_setspolynom gl th lc =
 
 module SectionPathSet =
   Set.Make(struct
-	     type t = section_path
+	     type t = full_path
 	     let compare = Pervasives.compare
 	   end)
 
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index bdec6bf45..1caa5db1c 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -20,15 +20,15 @@ let destructurate t =
   match Term.kind_of_term c, args with
     | Term.Const sp, args ->
 	Kapp (Names.string_of_id
-		(Nametab.id_of_global (Libnames.ConstRef sp)),
+		(Nametab.basename_of_global (Libnames.ConstRef sp)),
 	      args)
     | Term.Construct csp , args ->
 	Kapp (Names.string_of_id
-		(Nametab.id_of_global (Libnames.ConstructRef csp)),
+		(Nametab.basename_of_global (Libnames.ConstructRef csp)),
 	      args)
     | Term.Ind isp, args ->
 	Kapp (Names.string_of_id
-		(Nametab.id_of_global (Libnames.IndRef isp)),
+		(Nametab.basename_of_global (Libnames.IndRef isp)),
 	      args)
     | Term.Var id,[] -> Kvar(Names.string_of_id id)
     | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body)
@@ -46,7 +46,7 @@ let dest_const_apply t =
     | Term.Construct csp -> Libnames.ConstructRef csp
     | Term.Ind isp       -> Libnames.IndRef isp
     | _ -> raise Destruct
-  in  Nametab.id_of_global ref, args
+  in  Nametab.basename_of_global ref, args
 
 let logic_dir = ["Coq";"Logic";"Decidable"]
 
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 32f36ef85..24cb84ed5 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -352,18 +352,11 @@ let from_name = ref Spmap.empty
 
 let ring_for_carrier r = Cmap.find r !from_carrier
 let ring_for_relation rel = Cmap.find rel !from_relation
-let ring_lookup_by_name ref =
-  Spmap.find (Nametab.locate_obj (snd(qualid_of_reference ref))) !from_name
 
 
-let find_ring_structure env sigma l oname =
-  match oname, l with
-      Some rf, _ ->
-        (try ring_lookup_by_name rf
-        with Not_found ->
-          errorlabstrm "ring"
-            (str "found no ring named "++pr_reference rf))
-    | None, t::cl' ->
+let find_ring_structure env sigma l =
+  match l with
+    | t::cl' ->
         let ty = Retyping.get_type_of env sigma t in
         let check c =
           let ty' = Retyping.get_type_of env sigma c in
@@ -377,7 +370,7 @@ let find_ring_structure env sigma l oname =
           errorlabstrm "ring"
             (str"cannot find a declared ring structure over"++
              spc()++str"\""++pr_constr ty++str"\""))
-    | None, [] -> assert false
+    | [] -> assert false
 (*
         let (req,_,_) = dest_rel cl in
         (try ring_for_relation req
@@ -457,7 +450,7 @@ let (theory_to_obj, obj_to_theory) =
       open_function = (fun i o -> if i=1 then cache_th o);
       cache_function = cache_th;
       subst_function = subst_th;
-      classify_function = (fun (_,x) -> Substitute x);
+      classify_function = (fun x -> Substitute x);
       export_function = export_th }
 
 
@@ -835,7 +828,7 @@ let ring_lookup (f:glob_tactic_expr) lH rl t gl =
   let env = pf_env gl in
   let sigma = project gl in
   let rl = make_args_list rl t in
-  let e = find_ring_structure env sigma rl None in
+  let e = find_ring_structure env sigma rl in
   let rl = carg (make_term_list e.ring_carrier rl) in
   let lH = carg (make_hyp_list env lH) in
   let ring = ltac_ring_structure e in
@@ -941,20 +934,11 @@ let field_from_name = ref Spmap.empty
 
 let field_for_carrier r = Cmap.find r !field_from_carrier
 let field_for_relation rel = Cmap.find rel !field_from_relation
-let field_lookup_by_name ref =
-  Spmap.find (Nametab.locate_obj (snd(qualid_of_reference ref)))
-    !field_from_name
-
 
-let find_field_structure env sigma l oname =
+let find_field_structure env sigma l =
   check_required_library (cdir@["Field_tac"]);
-  match oname, l with
-      Some rf, _ ->
-        (try field_lookup_by_name rf
-        with Not_found ->
-          errorlabstrm "field"
-            (str "found no field named "++pr_reference rf))
-    | None, t::cl' ->
+  match l with
+    | t::cl' ->
         let ty = Retyping.get_type_of env sigma t in
         let check c =
           let ty' = Retyping.get_type_of env sigma c in
@@ -968,7 +952,7 @@ let find_field_structure env sigma l oname =
           errorlabstrm "field"
             (str"cannot find a declared field structure over"++
              spc()++str"\""++pr_constr ty++str"\""))
-    | None, [] -> assert false
+    | [] -> assert false
 (*        let (req,_,_) = dest_rel cl in
         (try field_for_relation req
         with Not_found ->
@@ -1046,7 +1030,7 @@ let (ftheory_to_obj, obj_to_ftheory) =
       open_function = (fun i o -> if i=1 then cache_th o);
       cache_function = cache_th;
       subst_function = subst_th;
-      classify_function = (fun (_,x) -> Substitute x);
+      classify_function = (fun x -> Substitute x);
       export_function = export_th }
 
 let field_equality r inv req =
@@ -1175,7 +1159,7 @@ let field_lookup (f:glob_tactic_expr) lH rl t gl =
   let env = pf_env gl in
   let sigma = project gl in
   let rl = make_args_list rl t in
-  let e = find_field_structure env sigma rl None in
+  let e = find_field_structure env sigma rl in
   let rl = carg (make_term_list e.field_carrier rl) in
   let lH = carg (make_hyp_list env lH) in
   let field = ltac_field_structure e in
diff --git a/plugins/subtac/equations.ml4 b/plugins/subtac/equations.ml4
index 5b76c9587..5ae15e00a 100644
--- a/plugins/subtac/equations.ml4
+++ b/plugins/subtac/equations.ml4
@@ -10,7 +10,7 @@
 (*i camlp4deps: "parsing/grammar.cma" i*)
 (*i camlp4use: "pa_extend.cmo" i*) 
 
-(* $Id: subtac_cases.ml 11198 2008-07-01 17:03:43Z msozeau $ *)
+(* $Id$ *)
 
 open Cases
 open Util
@@ -824,13 +824,13 @@ open Decl_kinds
 type equation = constr_expr * (constr_expr, identifier located) rhs
 
 let locate_reference qid =
-  match Nametab.extended_locate qid with
+  match Nametab.locate_extended qid with
     | TrueGlobal ref -> true
-    | SyntacticDef kn -> true
+    | SynDef kn -> true
 
 let is_global id =
   try 
-    locate_reference (make_short_qualid id)
+    locate_reference (qualid_of_ident id)
   with Not_found -> 
     false
 
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index 13e5e6d5f..1ac022159 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -15,7 +15,7 @@
 (* Utility Functions *)
 
 exception TwoModulesWhoseDirPathIsOneAPrefixOfTheOther;;
-let get_module_path_of_section_path path =
+let get_module_path_of_full_path path =
  let dirpath = fst (Libnames.repr_path path) in
  let modules = Lib.library_dp () :: (Library.loaded_libraries ()) in
   match
@@ -177,7 +177,7 @@ let uri_of_kernel_name tag =
 
 let uri_of_declaration id tag =
  let module LN = Libnames in
- let dir = LN.extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ()) in
+ let dir = LN.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ()) in
  let tokens = token_list_of_path dir id tag in
   "cic:/" ^ String.concat "/" tokens
 
@@ -468,14 +468,14 @@ print_endline "PASSATO" ; flush stdout ;
                 match g with
                    Libnames.ConstructRef ((induri,_),_)
                  | Libnames.IndRef (induri,_) ->
-                    Nametab.sp_of_global (Libnames.IndRef (induri,0))
+                    Nametab.path_of_global (Libnames.IndRef (induri,0))
                  | Libnames.VarRef id ->
                     (* Invariant: variables are never cooked in Coq *)
                     raise Not_found
-                 | _ -> Nametab.sp_of_global g
+                 | _ -> Nametab.path_of_global g
                in
                Dischargedhypsmap.get_discharged_hyps sp,
-               get_module_path_of_section_path sp
+               get_module_path_of_full_path sp
              with Not_found ->
                 (* no explicit substitution *)
                 [], Libnames.dirpath_of_string "dummy"
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 1ae186614..4a27c3247 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -102,7 +102,7 @@ let filter_params pvars hyps =
  in
   let cwd = Lib.cwd () in
   let cwdsp = Libnames.make_path cwd (Names.id_of_string "dummy") in
-  let modulepath = Cic2acic.get_module_path_of_section_path cwdsp in
+  let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in
    aux (Names.repr_dirpath modulepath) (List.rev pvars)
 ;;
 
@@ -118,7 +118,7 @@ let search_variables () =
  let module N = Names in
   let cwd = Lib.cwd () in
   let cwdsp = Libnames.make_path cwd (Names.id_of_string "dummy") in
-  let modulepath = Cic2acic.get_module_path_of_section_path cwdsp in
+  let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in
    let rec aux =
     function
        [] -> []