27 files changed, 125 insertions, 137 deletions
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index bdf4544f9..3b2dff70d 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -207,9 +207,7 @@ let recognize_number t =
  To use the constant Zplus, one must type "Lazy.force coq_Zplus"
  This is the right way to access to Coq constants in tactics ML code *)
 
-let constant dir id = 
-  Declare.global_qualified_reference
-    (make_path dir (id_of_string id) CCI)
+let constant dir s = Declare.global_qualified_reference (make_qualid dir s)
 
 (* fast_integer *)
 let coq_xH = lazy (constant ["fast_integer"] "xH")
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index 7aba0db66..3a431bc76 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -112,12 +112,8 @@ open Proof_type
   We do that lazily, because this code can be linked before
   the constants are loaded in the environment *)
 
-let constant sp id = 
-  Declare.global_qualified_reference
-    (make_path (dirpath (path_of_string sp)) (id_of_string id) CCI)
-(*
-  Declare.global_sp_reference (path_of_string sp) (id_of_string id)
-*)
+let constant dir s = Declare.global_qualified_reference (make_qualid [dir] s)
+
 let coq_Empty_vm = lazy (constant "#Quote#varmap.cci" "Empty_vm")
 let coq_Node_vm = lazy (constant "#Quote#varmap.cci" "Node_vm")
 let coq_varmap_find = lazy (constant "#Quote#varmap_find.cci" "varmap_find")
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 6080d7897..7b96983a7 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -25,8 +25,7 @@ open Quote;;
 let mt_evd = Evd.empty
 let constr_of com = Astterm.interp_constr mt_evd (Global.env()) com
 
-let constant dir id = 
-  Declare.global_qualified_reference (make_path dir (id_of_string id) CCI)
+let constant dir s = Declare.global_qualified_reference (make_qualid dir s)
 
 (* Ring_theory *)
 
diff --git a/kernel/names.ml b/kernel/names.ml
index 8205c564e..76f17525d 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -126,6 +126,15 @@ let kind_of_string = function
   | "obj" -> OBJ
   | _ -> invalid_arg "kind_of_string"
 
+(*s Section paths *)
+
+type qualid = string list * string
+
+let make_qualid p s = (p,s)
+let repr_qualid q = q
+
+let string_of_qualid (l,s) = String.concat "." (l@[s])
+let print_qualid (l,s) = prlist_with_sep (fun () -> pr_str ".") pr_str (l@[s])
 
 (*s Section paths *)
 
diff --git a/kernel/names.mli b/kernel/names.mli
index 323009011..3a380a42d 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -49,6 +49,17 @@ type dir_path = string list
 (* Printing of directory paths as ["#module#submodule"] *)
 val string_of_dirpath : dir_path -> string
 
+
+(*s Section paths *)
+
+type qualid
+
+val make_qualid : string list -> string -> qualid
+val repr_qualid : qualid -> string list * string
+
+val string_of_qualid : qualid -> string
+val print_qualid : qualid -> std_ppcmds
+
 (*s Section paths *)
 type section_path
 
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index a79dbcf3c..39223c726 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -60,7 +60,7 @@ type type_error =
   | WrongPredicateArity of constr * int * int
   | NeedsInversion of constr * constr
   (* Relocation error *)
-  | GlobalNotFound of section_path
+  | QualidNotFound of qualid
 
 exception TypeError of path_kind * env * type_error
 
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 9a2504ff8..68628c63c 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -64,7 +64,7 @@ type type_error =
   | WrongPredicateArity of constr * int * int
   | NeedsInversion of constr * constr
   (* Relocation error *)
-  | GlobalNotFound of section_path
+  | QualidNotFound of qualid
 
 exception TypeError of path_kind * env * type_error
 
diff --git a/library/declare.mli b/library/declare.mli
index 95aa8be8f..388580a87 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -83,10 +83,10 @@ val extract_instance : global_reference -> constr array -> constr array
 val constr_of_reference :
   'a Evd.evar_map -> Environ.env -> global_reference -> constr
 
-val global_qualified_reference : section_path -> constr
+val global_qualified_reference : qualid -> constr
 val global_reference : path_kind -> identifier -> constr
 
-val construct_qualified_reference : Environ.env -> section_path -> constr
+val construct_qualified_reference : Environ.env -> qualid -> constr
 val construct_reference : Environ.env -> path_kind -> identifier -> constr
 
 val is_global : identifier -> bool
diff --git a/library/nametab.ml b/library/nametab.ml
index 8e15870e0..c45e7d93e 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -7,65 +7,66 @@ open Libobject
 open Declarations
 open Term
 
-type cci_table = global_reference Idmap.t
-type obj_table = (section_path * obj) Idmap.t
+type cci_table = global_reference Stringmap.t
+type obj_table = (section_path * obj) Stringmap.t
 type mod_table = module_contents Stringmap.t
 and module_contents = Closed of cci_table * obj_table * mod_table
 
 let mod_tab = ref (Stringmap.empty : mod_table)
-let cci_tab = ref (Idmap.empty : cci_table)
-let obj_tab = ref (Idmap.empty : obj_table)
+let cci_tab = ref (Stringmap.empty : cci_table)
+let obj_tab = ref (Stringmap.empty : obj_table)
 
-let sp_of_id _ id = Idmap.find id !cci_tab
+let sp_of_id _ id = Stringmap.find (string_of_id id) !cci_tab
 
 let constant_sp_of_id id =
-  match Idmap.find id !cci_tab with
+  match Stringmap.find (string_of_id id) !cci_tab with
     | ConstRef sp -> sp
     | _ -> raise Not_found
 
-let push_cci id sp = cci_tab := Idmap.add id sp !cci_tab
-let push_obj id sp = obj_tab := Idmap.add id sp !obj_tab
-let push_module id mc = mod_tab := Stringmap.add id mc !mod_tab
+let push_cci s sp = cci_tab := Stringmap.add s sp !cci_tab
+let push_obj s sp = obj_tab := Stringmap.add s sp !obj_tab
+let push_module s mc = mod_tab := Stringmap.add s mc !mod_tab
 
-let push = push_cci
+let push_object id = push_obj (string_of_id id)
+let push id = push_cci (string_of_id id) 
 
-let locate sp =
-  let (dir,id,_) = repr_path sp in
+let locate qid =
+  let (dir,id) = repr_qualid qid in
   let rec search (ccitab,modtab) = function
     | id :: dir' ->
 	let (Closed (ccitab, _, modtab)) = Stringmap.find id modtab in
 	search (ccitab,modtab) dir'
-    | [] -> Idmap.find id ccitab
+    | [] -> Stringmap.find id ccitab
   in search (!cci_tab,!mod_tab) dir
 
-let locate_obj sp =
-  let (dir,id,_) = repr_path sp in
+let locate_obj qid =
+  let (dir,id) = repr_qualid qid in
   let rec search (objtab,modtab) = function
     | id :: dir' ->
 	let (Closed (_, objtab, modtab)) = Stringmap.find id modtab in
 	search (objtab,modtab) dir'
-    | [] -> Idmap.find id objtab
+    | [] -> Stringmap.find id objtab
   in search (!obj_tab,!mod_tab) dir
 
-let locate_constant sp =
-  match locate sp with
+let locate_constant qid =
+  match locate qid with
     | ConstRef sp -> sp
     | _ -> raise Not_found
 
-let open_module_contents id =
-  let (Closed (ccitab,objtab,modtab)) = Stringmap.find id !mod_tab in
-  Idmap.iter push_cci ccitab;
-  Idmap.iter (fun _ -> Libobject.open_object) objtab;
+let open_module_contents s =
+  let (Closed (ccitab,objtab,modtab)) = Stringmap.find s !mod_tab in
+  Stringmap.iter push_cci ccitab;
+  Stringmap.iter (fun _ -> Libobject.open_object) objtab;
   Stringmap.iter push_module modtab
 
 (* Registration as a global table and roolback. *)
     
 let init () =
-  cci_tab := Idmap.empty;
-  obj_tab := Idmap.empty;
+  cci_tab := Stringmap.empty;
+  obj_tab := Stringmap.empty;
   mod_tab := Stringmap.empty;
 
-type frozen = cci_table Idmap.t * obj_table Idmap.t * mod_table Stringmap.t
+type frozen = cci_table Stringmap.t * obj_table Stringmap.t * mod_table Stringmap.t
 
 let freeze () = (!cci_tab, !obj_tab, !mod_tab)
 		  
diff --git a/library/nametab.mli b/library/nametab.mli
index 68e272740..9a90a70b8 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -10,13 +10,13 @@ open Term
 (* This module contains the table for globalization, which associates global
    names (section paths) to identifiers. *)
 
-type cci_table = global_reference Idmap.t
-type obj_table = (section_path * Libobject.obj) Idmap.t
+type cci_table = global_reference Stringmap.t
+type obj_table = (section_path * Libobject.obj) Stringmap.t
 type mod_table = module_contents Stringmap.t
 and module_contents = Closed of cci_table * obj_table * mod_table
 
 val push : identifier -> global_reference -> unit
-val push_obj : identifier -> (section_path * Libobject.obj) -> unit
+val push_object : identifier -> (section_path * Libobject.obj) -> unit
 val push_module : string -> module_contents -> unit
 
 val sp_of_id : path_kind -> identifier -> global_reference
@@ -24,9 +24,11 @@ val sp_of_id : path_kind -> identifier -> global_reference
 (* This returns the section path of a constant or fails with [Not_found] *)
 val constant_sp_of_id : identifier -> section_path
 
-val locate : section_path -> global_reference
-val locate_obj : section_path -> (section_path * Libobject.obj)
-val locate_constant : section_path -> constant_path
+val locate : qualid -> global_reference
+val locate_obj : qualid -> (section_path * Libobject.obj)
+val locate_constant : qualid -> constant_path
 
 val open_module_contents : string -> unit
 
+
+
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index c4c7a3e45..c89ec4a53 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -178,50 +178,18 @@ let ref_from_constr c = match kind_of_term c with
    [vars2] is the set of global variables, env is the set of variables
    abstracted until this point *)
 
-let ast_to_var env (vars1,vars2) loc id =
+let ast_to_var env (vars1,vars2) loc s =
+  let id = id_of_string s in
   let imp = 
-    if Idset.mem id env or List.mem (string_of_id id) vars1
+    if Idset.mem id env or List.mem s vars1
     then []
     else
       let _ = lookup_id id vars2 in
       (* Car Fixpoint met les fns d�finies tmporairement comme vars de sect *)
-      try implicits_of_global (Nametab.locate (make_path [] id CCI))
+      try implicits_of_global (Nametab.locate (make_qualid [] s))
       with _ -> []
   in RVar (loc, id), imp
 
-(*
-let ast_to_global_ref loc qualid =
-  try
-    let ref = Nametab.locate qualid in
-    RRef (loc, ref), implicits_of_global ref
-  with Not_found ->
-    let sp = Syntax_def.locate_syntactic_definition qualid in
-    Syntax_def.search_syntactic_definition sp, []
-
-let ast_to_ref env (vars1,vars2) loc s =
-  let id = ident_of_nvar loc s in
-  try
-    let id, imp = ast_to_var env (vars1,vars2) loc s in
-    RVar (loc, id), imp
-  with Not_found ->
-  try
-    ast_to_global_ref loc (make_path [] id CCI)
-  with Not_found ->
-    error_var_not_found_loc loc CCI id
-
-let ast_to_qualid env vars loc p =
-  let outnvar = function
-    | Nvar (loc,s) -> s
-    | _ -> anomaly "bad-formed path" in
-  match p with
-    | [] -> anomaly "ast_to_qualid: Empty qualified id"
-    | [s] -> ast_to_ref env vars loc (outnvar s)
-    | l -> 
-	let p,r = list_chop (List.length l -1) (List.map outnvar l) in
-	let id = id_of_string (List.hd r) in
-	ast_to_global_ref loc (make_path p id CCI)
-*)
-
 let interp_qualid p =
   let outnvar = function
     | Nvar (loc,s) -> s
@@ -230,32 +198,32 @@ let interp_qualid p =
     | [] -> anomaly "interp_qualid: empty qualified identifier"
     | l -> 
 	let p, r = list_chop (List.length l -1) (List.map outnvar l) in
-	let id = id_of_string (List.hd r) in
-	make_path p id CCI
+	make_qualid p (List.hd r)
 
-let rawconstr_of_var env vars loc id =
+let rawconstr_of_var env vars loc s =
   try
-    ast_to_var env vars loc id
+    ast_to_var env vars loc s
   with Not_found ->
-    error_var_not_found_loc loc CCI id
+    error_var_not_found_loc loc CCI (id_of_string s)
 
-let rawconstr_of_qualid env vars loc sp =
+let rawconstr_of_qualid env vars loc qid =
   (* Is it a bound variable? *)
   try
-    if dirpath sp <> [] then raise Not_found;
-    ast_to_var env vars loc (basename sp)
+    match repr_qualid qid with
+      | [],s -> ast_to_var env vars loc s
+      | _ -> raise Not_found
   with Not_found ->
   (* Is it a global reference? *)
   try
-    let ref = Nametab.locate sp in
+    let ref = Nametab.locate qid in
     RRef (loc, ref), implicits_of_global ref
   with Not_found ->
   (* Is it a reference to a syntactic definition? *)
   try
-    let sp = Syntax_def.locate_syntactic_definition sp in
+    let sp = Syntax_def.locate_syntactic_definition qid in
     Syntax_def.search_syntactic_definition sp, []
   with Not_found ->
-    error_global_not_found_loc loc sp
+    error_global_not_found_loc loc qid
 
 let mkLambdaC (x,a,b) = ope("LAMBDA",[a;slam(Some (string_of_id x),b)])
 let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b))
@@ -338,7 +306,7 @@ let check_capture loc s ty = function
 let ast_to_rawconstr sigma env allow_soapp lvar =
   let rec dbrec env = function
     | Nvar(loc,s) ->
-	fst (rawconstr_of_var env lvar loc (ident_of_nvar loc s))
+	fst (rawconstr_of_var env lvar loc s)
 
     | Node(loc,"QUALID", l) ->
 	fst (rawconstr_of_qualid env lvar loc (interp_qualid l))
@@ -549,18 +517,19 @@ let ast_adjust_consts sigma =
         else if Idset.mem id env then ast
         else 
 	  (try
-	     ast_of_qualid loc (make_path [] id CCI)
+	     ast_of_qualid loc (make_qualid [] s)
 	   with Not_found ->
 	     warning ("Could not globalize " ^ s); ast)
     | Node (loc, "QUALID", p) as ast ->
 	(match p with
 	   | [Nvar (_,s) as v] when isMeta s -> v
 	   | _ ->
-	       let sp = interp_qualid p in
+	       let qid = interp_qualid p in
 	       try
-		 ast_of_qualid loc sp
+		 ast_of_qualid loc qid
 	       with Not_found -> 
-		 warning ("Could not globalize " ^ (string_of_path sp)); ast)
+		 warning ("Could not globalize " ^ (string_of_qualid qid));
+		 ast)
     | Slam (loc, None, t) -> Slam (loc, None, dbrec env t)
     | Slam (loc, Some na, t) ->
         let env' = Idset.add (id_of_string na) env in
diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index 703d9de19..d1e98002e 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -57,9 +57,9 @@ val globalize_ast    : Coqast.t -> Coqast.t
 
 (* This transforms args of a qualid keyword into a qualified ident *)
 (* it does no relocation *)
-val interp_qualid : Coqast.t list -> section_path
+val interp_qualid : Coqast.t list -> qualid
 
-val ast_of_qualid : Coqast.loc -> section_path -> Coqast.t
+val ast_of_qualid : Coqast.loc -> qualid -> Coqast.t
 
 (* Translation rules from V6 to V7:
 
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index e59e37e64..6f2011eb8 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -415,7 +415,7 @@ let print_name name =
     [< print_named_decl (name,c,typ) >]
   with Not_found ->
   try
-    let sp = Syntax_def.locate_syntactic_definition (make_path [] name CCI) in
+    let sp = Syntax_def.locate_syntactic_definition (make_qualid [] str) in
     print_syntactic_def true " = " sp
   with Not_found ->
     error (str ^ " not a defined object")
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 594f3fc9e..3a6897d98 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -13,8 +13,8 @@ let raise_pretype_error (loc,k,ctx,te) =
 let error_var_not_found_loc loc k s =
   raise_pretype_error (loc,k, Global.env() (*bidon*), VarNotFound s)
 
-let error_global_not_found_loc loc sp =
-  raise_pretype_error (loc,CCI, Global.env() (*bidon*), GlobalNotFound sp)
+let error_global_not_found_loc loc q =
+  raise_pretype_error (loc,CCI, Global.env() (*bidon*), QualidNotFound q)
 
 let error_cant_find_case_type_loc loc env expr =
   raise_pretype_error (loc, CCI, env, CantFindCaseType expr)
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index c670e1f97..e91ec8a45 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -17,7 +17,7 @@ val error_var_not_found_loc :
   loc -> path_kind -> identifier -> 'a
 
 val error_global_not_found_loc :
-  loc -> section_path -> 'a
+  loc -> qualid -> 'a
 
 val error_cant_find_case_type_loc : 
   loc -> env -> constr -> 'a
diff --git a/pretyping/syntax_def.ml b/pretyping/syntax_def.ml
index 0038b69d5..f90627f7e 100644
--- a/pretyping/syntax_def.ml
+++ b/pretyping/syntax_def.ml
@@ -35,7 +35,7 @@ let (in_syntax_constant, out_syntax_constant) =
 let _ =
   cache_syntax_constant := fun (sp,c) ->
     add_syntax_constant sp c;
-    Nametab.push_obj (basename sp) (sp, in_syntax_constant c)
+    Nametab.push_object (basename sp) (sp, in_syntax_constant c)
 
 let declare_syntactic_definition id c =
   let _ = add_leaf id CCI (in_syntax_constant c) in ()
diff --git a/pretyping/syntax_def.mli b/pretyping/syntax_def.mli
index 48a996991..7a1116ba0 100644
--- a/pretyping/syntax_def.mli
+++ b/pretyping/syntax_def.mli
@@ -12,6 +12,6 @@ val declare_syntactic_definition : identifier -> rawconstr -> unit
 
 val search_syntactic_definition : section_path -> rawconstr
 
-val locate_syntactic_definition : section_path -> section_path
+val locate_syntactic_definition : qualid -> section_path
 
 
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index c2dcf0bec..29daa7965 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -136,14 +136,14 @@ let look_for_interp = Hashtbl.find interp_tab
 
 (* Globalizes the identifier *)
 let glob_const_nvar loc id =
-  let sp = make_path [] id CCI in
+  let qid = make_qualid [] (string_of_id id) in
   try
-    match Nametab.locate sp with
+    match Nametab.locate qid with
       | ConstRef sp -> sp
-      | _ -> error ((string_of_path sp) ^ " does not denote a constant")
+      | _ -> error ((string_of_qualid qid) ^ " does not denote a constant")
   with
     | Not_found ->
-	Pretype_errors.error_global_not_found_loc loc sp
+	Pretype_errors.error_global_not_found_loc loc qid
 
 
 (* Summary and Object declaration *)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 9228013be..7d59ecf21 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -669,8 +669,7 @@ let h_discrHyp   = hide_ident_tactic  "DiscrHyp"   discrHyp
 let existS_pattern = put_pat mmk "(existS ?1 ?2 ?3 ?4)"
 let existT_pattern = put_pat mmk "(existT ?1 ?2 ?3 ?4)"
 
-let constant dir id = 
-  Declare.global_qualified_reference (make_path dir (id_of_string id) CCI)
+let constant dir s = Declare.global_qualified_reference (make_qualid dir s)
 
 let build_sigma_set () =
   { proj1 = constant ["Specif"] "projS1";
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4f4afec9b..3b152c27c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1516,8 +1516,7 @@ let contradiction_on_hyp id gl =
   else 
     error "Not a contradiction"
 
-let constant dir id = 
-  Declare.global_qualified_reference (make_path dir (id_of_string id) CCI)
+let constant dir s = Declare.global_qualified_reference (make_qualid dir s)
 
 let coq_False = lazy (constant ["Logic"] "False")
 let coq_not = lazy (constant ["Logic"] "not")
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 866d09f7d..3c702e2b4 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -247,8 +247,10 @@ let push_inductive_names ccitab sp mie =
 	 let _,ccitab =
 	   List.fold_left
 	     (fun (p,ccitab) x ->
-		(p+1,Idmap.add x (ConstructRef (indsp,p)) ccitab))
-	     (1,Idmap.add id (IndRef indsp) ccitab)
+		(p+1,
+		 Stringmap.add (string_of_id x) (ConstructRef (indsp,p)) 
+		   ccitab))
+	     (1,Stringmap.add (string_of_id id) (IndRef indsp) ccitab)
 	     cnames in
 	 (n+1,ccitab))
       (0,ccitab)
@@ -259,7 +261,8 @@ let rec process_object (ccitab, objtab, modtab as tabs) = function
   | sp,Leaf obj -> 
       begin match object_tag obj with
 	| "CONSTANT" | "PARAMETER" ->
-            (Idmap.add (basename sp) (ConstRef sp) ccitab,objtab,modtab)
+            (Stringmap.add (string_of_id (basename sp))
+	       (ConstRef sp) ccitab,objtab,modtab)
 	| "INDUCTIVE" ->
 	    let mie = out_inductive obj in
 	    (push_inductive_names ccitab sp mie, objtab, modtab)
@@ -270,7 +273,9 @@ let rec process_object (ccitab, objtab, modtab as tabs) = function
         (* ou quelque chose comme cela *)
 	| "CLASS" | "COERCION" | "STRUCTURE" | "OBJDEF1" | "SYNTAXCONSTANT"
 	| _ ->
-	    (ccitab, Idmap.add (basename sp) (sp,obj) objtab, modtab)
+	    (ccitab,
+	     Stringmap.add (string_of_id (basename sp)) (sp,obj) objtab,
+	     modtab)
       end 
   | sp,ClosedSection (export,_,seg,contents) ->
       let id = string_of_id (basename sp) in
@@ -279,7 +284,8 @@ let rec process_object (ccitab, objtab, modtab as tabs) = function
 
 and module_contents seg =
   let ccitab, objtab, modtab =
-    List.fold_left process_object (Idmap.empty, Idmap.empty, Stringmap.empty)
+    List.fold_left process_object
+      (Stringmap.empty, Stringmap.empty, Stringmap.empty)
       seg
   in Nametab.Closed (ccitab, objtab, modtab)
 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 449b7bc1e..afaf5a2d4 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -279,8 +279,8 @@ let explain_var_not_found k ctx id =
      'sPC ; 'sTR "was not found"; 
      'sPC ; 'sTR "in the current"; 'sPC ; 'sTR "environment" >]
 
-let explain_global_not_found k ctx sp = 
-  [< 'sTR "The reference"; 'sPC; 'sTR (string_of_path sp);
+let explain_global_not_found k ctx q = 
+  [< 'sTR "The reference"; 'sPC; print_qualid q;
      'sPC ; 'sTR "was not found"; 
      'sPC ; 'sTR "in the current"; 'sPC ; 'sTR "environment" >]
 
@@ -360,7 +360,7 @@ let explain_type_error k ctx = function
       explain_not_clean k ctx n c
   | VarNotFound id ->
       explain_var_not_found k ctx id
-  | GlobalNotFound sp ->
+  | QualidNotFound sp ->
       explain_global_not_found k ctx sp
   | UnexpectedType (actual,expected) ->
       explain_unexpected_type k ctx actual expected
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index d1bada0c2..eb7543f3d 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -219,7 +219,7 @@ let add_infix assoc n inf pr =
       [< 'sTR"Associativity Precedence must be 6,7,8 or 9." >];
   (* check the grammar entry *)
   let prefast = Astterm.ast_of_qualid dummy_loc pr in
-  let prefname = (Names.string_of_path pr)^"_infix" in
+  let prefname = (Names.string_of_qualid pr)^"_infix" in
   let gram_rule = gram_infix assoc n (split inf) prefname prefast in
   (* check the syntax entry *)
   let syntax_rule = infix_syntax_entry assoc n inf prefname prefast in
@@ -267,7 +267,7 @@ let distfix assoc n sl fname astf  =
   }
 
 let add_distfix a n df f =
-  let fname = (Names.string_of_path f)^"_distfix" in
+  let fname = (Names.string_of_qualid f)^"_distfix" in
   let astf = Astterm.ast_of_qualid dummy_loc f in
   Lib.add_anonymous_leaf (inInfix(distfix a n (split df) fname astf, []))
 
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 18b0a7d98..e3d9e593d 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -13,8 +13,7 @@ val add_syntax_obj : string -> Coqast.t list -> unit
 val add_grammar_obj : string -> Coqast.t list -> unit
 val add_token_obj : string -> unit
 
-val add_infix : Gramext.g_assoc option -> int -> string -> section_path -> unit
-val add_distfix : Gramext.g_assoc option -> int -> string -> section_path
-  -> unit
+val add_infix : Gramext.g_assoc option -> int -> string -> qualid -> unit
+val add_distfix : Gramext.g_assoc option -> int -> string -> qualid -> unit
 
 val print_grammar : string -> string -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 118ba6616..6363decfe 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -113,18 +113,18 @@ let locate_file f =
     mSG (hOV 0 [< 'sTR"Can't find file"; 'sPC; 'sTR f; 'sPC;
 		  'sTR"on loadpath"; 'fNL >])
 
-let locate_sp sp =
+let locate_qualid qid =
   try
-    let ref = Nametab.locate sp in
+    let ref = Nametab.locate qid in
     mSG
       [< 'sTR (string_of_path (sp_of_global (Global.env()) ref)); 'fNL >]
   with Not_found -> 
   try
     mSG
-      [< 'sTR (string_of_path (Syntax_def.locate_syntactic_definition sp));
+      [< 'sTR (string_of_path (Syntax_def.locate_syntactic_definition qid));
 	 'fNL >]
   with Not_found ->
-    error ((string_of_path sp) ^ " not a defined object")
+    error ((string_of_qualid qid) ^ " not a defined object")
 
 let print_loadpath () =
   let l = get_load_path () in
@@ -158,7 +158,7 @@ let _ =
 let _ = 
   add "Locate"
     (function 
-       | [VARG_QUALID sp] -> (fun () -> locate_sp sp)
+       | [VARG_QUALID qid] -> (fun () -> locate_qualid qid)
        | _  -> bad_vernac_args "Locate")
 
 (* For compatibility *)
@@ -885,12 +885,12 @@ let _ =
 let _ =
   add "SEARCH"
     (function 
-       | [VARG_QUALID q] ->
+       | [VARG_QUALID qid] ->
 	   (fun () ->
 	      let ref =
-		try Nametab.locate q
+		try Nametab.locate qid
 		with Not_found ->
-		  Pretype_errors.error_global_not_found_loc loc q
+		  Pretype_errors.error_global_not_found_loc loc qid
 	      in 
 	      search_by_head ref)
        | _ -> bad_vernac_args "SEARCH")
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index fd41ae5d2..a6538bc1b 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -24,7 +24,7 @@ type vernac_arg =
   | VARG_NUMBER of int
   | VARG_NUMBERLIST of int list
   | VARG_IDENTIFIER of identifier
-  | VARG_QUALID of section_path
+  | VARG_QUALID of qualid
   | VARG_CONSTANT of constant_path
   | VCALL of string * vernac_arg list
   | VARG_CONSTR of Coqast.t
diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli
index a83e452eb..4fe1b54c9 100644
--- a/toplevel/vernacinterp.mli
+++ b/toplevel/vernacinterp.mli
@@ -20,7 +20,7 @@ type vernac_arg =
   | VARG_NUMBER of int
   | VARG_NUMBERLIST of int list
   | VARG_IDENTIFIER of identifier
-  | VARG_QUALID of section_path
+  | VARG_QUALID of qualid
   | VARG_CONSTANT of constant_path
   | VCALL of string * vernac_arg list
   | VARG_CONSTR of Coqast.t