Modules dans COQ\!\!\!\!

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

31 files changed, 491 insertions, 368 deletions

diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index dbae1fce5a..1a0d4dc41a 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -229,7 +229,7 @@ let correctness_hook _ ref =
   register pf_id None
 
 let correctness s p opttac =
-  Library.check_required_module ["Coq";"correctness";"Correctness"];
+  Library.check_required_library ["Coq";"correctness";"Correctness"];
   Pmisc.reset_names();
   let p,oc,cty,v = coqast_of_prog p in
   let env = Global.env () in
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 139f849c86..c7f0a97d9a 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -16,9 +16,10 @@ open Table
 open Mlutil
 open Extraction
 open Ocaml
-open Nametab
+open Libnames
 open Util
 open Declare
+open Nametab
 
 (*s Modules considerations *)
 
@@ -34,7 +35,7 @@ let qualid_of_dirpath d =
       
 let is_long_module d r = 
   let dir = repr_dirpath d 
-  and dir' = repr_dirpath (dirpath (sp_of_r r)) in 
+  and dir' = repr_dirpath (fst (decode_kn (kn_of_r r))) in 
   let l = List.length dir 
   and l' = List.length dir' in 
   if l' < l then false 
@@ -106,7 +107,7 @@ let cache r f =
 
 module ToplevelParams = struct
   let globals () = Idset.empty
-  let rename_global r _ = Termops.id_of_global (Global.env()) r
+  let rename_global r _ = id_of_global None r
   let pp_global r _ _ = Printer.pr_global r
 end
 
@@ -124,7 +125,7 @@ module MonoParams = struct
   let rename_global r upper = 
     cache r
       (fun r -> 
-	 let id = Termops.id_of_global (Global.env()) r in
+	 let id = id_of_global None r in
 	 rename_global_id 
 	   (if upper || (is_construct r) 
 	    then uppercase_id id else lowercase_id id))
@@ -143,7 +144,7 @@ module ModularParams = struct
 
   let clash r id = 
     try 
-      let _ = locate (make_qualid (dirpath (sp_of_r r)) id)
+      let _ = locate (make_qualid (fst (decode_kn (kn_of_r r))) id)
       in true
     with _ -> false
 
@@ -160,7 +161,7 @@ module ModularParams = struct
   let rename_global r upper =
     cache r 
       (fun r -> 
-	 let id = Termops.id_of_global (Global.env()) r in 
+	 let id = id_of_global None r in 
 	 if upper || (is_construct r) then 
 	   rename_global_id r id (uppercase_id id) "Coq_"
 	 else rename_global_id r id (lowercase_id id) "coq_")
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
index 299ed508cf..9ebb110697 100644
--- a/contrib/extraction/common.mli
+++ b/contrib/extraction/common.mli
@@ -12,7 +12,7 @@ open Pp
 open Miniml
 open Mlutil
 open Names
-open Nametab
+open Libnames
 
 val is_long_module : dir_path -> global_reference -> bool
 
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 206de8a28a..d04a65fde6 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -18,6 +18,7 @@ open Extraction
 open Miniml
 open Table
 open Mlutil
+open Libnames
 open Nametab
 open Vernacinterp
 open Common
@@ -83,12 +84,12 @@ let check_modules m =
   We just keep constants and inductives. *)
 
 let extract_module m =
-  let seg = Library.module_segment (Some m) in
+  let seg = Declaremods.module_objects (MPfile m) in
   let get_reference = function
-    | sp, Leaf o ->
+    | (_,kn), Leaf o ->
 	(match Libobject.object_tag o with
-	   | "CONSTANT" | "PARAMETER" -> ConstRef sp
-	   | "INDUCTIVE" -> IndRef (sp,0)
+	   | "CONSTANT" | "PARAMETER" -> ConstRef kn
+	   | "INDUCTIVE" -> IndRef (kn,0)
 	   | _ -> failwith "caught")
     | _ -> failwith "caught"
   in
@@ -204,7 +205,7 @@ let print_user_extract r =
 let decl_in_r r0 = function 
   | Dterm (r,_) -> r = r0
   | Dtype (r,_,_) -> r = r0
-  | Dind ((_,r,_)::_, _) -> sp_of_r r = sp_of_r r0
+  | Dind ((_,r,_)::_, _) -> kn_of_r r = kn_of_r r0
   | Dind ([],_) -> false
   | DdummyType r -> r = r0
   | DcustomTerm (r,_) ->  r = r0 
diff --git a/contrib/extraction/extract_env.mli b/contrib/extraction/extract_env.mli
index e019df342b..2151618982 100644
--- a/contrib/extraction/extract_env.mli
+++ b/contrib/extraction/extract_env.mli
@@ -12,7 +12,7 @@
 
 open Util
 open Names
-open Nametab
+open Libnames
 
 val extraction : qualid located -> unit
 val extraction_rec : qualid located list -> unit
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 8b842c5b5e..f574cecae3 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -26,6 +26,7 @@ open Table
 open Mlutil
 open Closure
 open Summary
+open Libnames
 open Nametab
 (*i*)
 
@@ -91,13 +92,13 @@ let add_constructor c e = constructor_table := Gmap.add c e !constructor_table
 let lookup_constructor c = Gmap.find c !constructor_table
 
 let constant_table = 
-  ref (Gmap.empty : (section_path, ml_decl) Gmap.t)
-let add_constant sp d = constant_table := Gmap.add sp d !constant_table
-let lookup_constant sp = Gmap.find sp !constant_table
+  ref (Gmap.empty : (kernel_name, ml_decl) Gmap.t)
+let add_constant kn d = constant_table := Gmap.add kn d !constant_table
+let lookup_constant kn = Gmap.find kn !constant_table
 
-let signature_table = ref (Gmap.empty : (section_path, signature) Gmap.t)
-let add_signature sp s = signature_table := Gmap.add sp s !signature_table
-let lookup_signature sp = Gmap.find sp !signature_table 
+let signature_table = ref (Gmap.empty : (kernel_name, signature) Gmap.t)
+let add_signature kn s = signature_table := Gmap.add kn s !signature_table
+let lookup_signature kn = Gmap.find kn !signature_table 
 
 (* Tables synchronization. *)
 
@@ -116,15 +117,15 @@ let _ = declare_summary "Extraction tables"
 
 (*S Warning and Error messages. *)
 
-let axiom_error_message sp =
+let axiom_error_message kn =
   errorlabstrm "axiom_message"
     (str "You must specify an extraction for axiom" ++ spc () ++ 
-       pr_sp sp ++ spc () ++ str "first.")
+       pr_kn kn ++ spc () ++ str "first.")
 
-let axiom_warning_message sp = 
+let axiom_warning_message kn = 
   Options.if_verbose warn 
     (str "This extraction depends on logical axiom" ++ spc () ++ 
-     pr_sp sp ++ str "." ++ spc() ++ 
+     pr_kn kn ++ str "." ++ spc() ++ 
      str "Having false logical axiom in the environment when extracting" ++ 
      spc () ++ str "may lead to incorrect or non-terminating ML terms.")
     
@@ -140,7 +141,7 @@ let type_of env c = Retyping.get_type_of env none (strip_outer_cast c)
 
 let sort_of env c = Retyping.get_sort_family_of env none (strip_outer_cast c)
 
-let is_axiom sp = (Global.lookup_constant sp).const_body = None
+let is_axiom kn = (Global.lookup_constant kn).const_body = None
 
 (*s [flag_of_type] transforms a type [t] into a [flag]. 
   Really important function. *)
@@ -191,12 +192,12 @@ let rec type_sign_vl env c =
 
 (*s Function recording signatures of section paths. *)
 
-let signature_of_sp sp = 
-  try lookup_signature sp
+let signature_of_kn kn = 
+  try lookup_signature kn
   with Not_found -> 
     let env = Global.env () in 
-    let s = term_sign env (constant_type env sp)
-    in add_signature sp s; s
+    let s = term_sign env (constant_type env kn)
+    in add_signature kn s; s
 
 (*S Management of type variable contexts. *)
 
@@ -261,16 +262,16 @@ let rec extract_type env db c args =
 	   | _ -> 
 	       let n' = List.nth db (n-1) in 
 	       if n' = 0 then Tunknown else Tvar n')
-    | Const sp ->
-	let t = constant_type env sp in 
+    | Const kn ->
+	let t = constant_type env kn in 
 	(match flag_of_type env t with 
 	   | (Info,Arity) -> 
-	       extract_type_app env db (ConstRef sp, type_sign env t) args
+	       extract_type_app env db (ConstRef kn, type_sign env t) args
 	   | (Info,_) -> Tunknown
 	   | (Logic,_) -> Tdummy)
-    | Ind spi ->
-	(match extract_inductive spi with 
-	   | Iml (si,_) -> extract_type_app env db (IndRef spi,si) args
+    | Ind kni ->
+	(match extract_inductive kni with 
+	   | Iml (si,_) -> extract_type_app env db (IndRef kni,si) args
 	   | Iprop -> Tdummy)
     | Sort _ -> Tdummy 
     | Case _ | Fix _ | CoFix _ -> Tunknown
@@ -341,8 +342,8 @@ and extract_constructor (((sp,_),_) as c) =
   extract_mib sp;
   lookup_constructor c
 
-and extract_mib sp =
-  let ind = (sp,0) in
+and extract_mib kn =
+  let ind = (kn,0) in
   if not (Gmap.mem ind !inductive_table) then begin
     let (mib,mip) = Global.lookup_inductive ind in
     let env = Global.env () in 
@@ -353,7 +354,7 @@ and extract_mib sp =
     (* First pass: we store inductive signatures together with *)
     (* their type var list. *)
     for i = 0 to mib.mind_ntypes - 1 do
-      let ip = (sp,i) in 
+      let ip = (kn,i) in 
       let (mib,mip) = Global.lookup_inductive ip in 
       if mip.mind_sort = (Prop Null) then 
 	add_inductive ip Iprop
@@ -364,7 +365,7 @@ and extract_mib sp =
     done;
     (* Second pass: we extract constructors *)
     for i = 0 to mib.mind_ntypes - 1 do
-      let ip = (sp,i) in
+      let ip = (kn,i) in
       let (mib,mip) = Global.lookup_inductive ip in
       match lookup_inductive ip with 
 	| Iprop -> 
@@ -400,11 +401,11 @@ let is_singleton_inductive ind =
   (mib.mind_ntypes = 1) &&
   (Array.length mip.mind_consnames = 1) && 
   match extract_constructor (ind,1) with 
-    | Cml ([mlt],_,_)-> not (type_mem_sp (fst ind) mlt)
+    | Cml ([mlt],_,_)-> not (type_mem_kn (fst ind) mlt)
     | _ -> false
           
-let is_singleton_constructor ((sp,i),_) = 
-  is_singleton_inductive (sp,i) 
+let is_singleton_constructor ((kn,i),_) = 
+  is_singleton_inductive (kn,i) 
 
 (*S Modification of the signature of terms. *)
 
@@ -465,9 +466,9 @@ let rec extract_real_args env args s =
 
 (*s Abstraction of an constant. *)
 
-and apply_constant env sp args = 
-  let head = MLglob (ConstRef sp) in 
-  let s = signature_of_sp sp in 
+and apply_constant env kn args = 
+  let head = MLglob (ConstRef kn) in 
+  let s = signature_of_kn kn in 
   let ls = List.length s in 
   let la = Array.length args in 
   if ls = 0 then begin
@@ -552,15 +553,15 @@ and extract_term env c =
     | App (f,a) ->
 	(match kind_of_term (strip_outer_cast f) with 
 	   | App _ -> assert false 
-      	   | Const sp -> apply_constant env sp a 
+      	   | Const kn -> apply_constant env kn a 
 	   | Construct cp -> apply_constructor env cp a
 	   | _ -> 
 	       let mlargs = 
 		 Array.fold_right 
 		   (fun a l -> (extract_constr_to_term env a) :: l) a []
 	       in MLapp (extract_term env f, mlargs))
-    | Const sp ->
-	apply_constant env sp [||]
+    | Const kn ->
+	apply_constant env kn [||]
     | Construct cp ->
 	apply_constructor env cp [||]
     | Case ({ci_ind=ip},_,c,br) ->
@@ -652,17 +653,17 @@ and extract_constr_to_term_wt env c t =
 
 (*s From a constant to a ML declaration. *)
 
-let extract_constant sp r = 
+let extract_constant kn r = 
   let env = Global.env() in    
-  let cb = Global.lookup_constant sp in
+  let cb = Global.lookup_constant kn in
   let typ = cb.const_type in
   match cb.const_body with
     | None -> (* A logical axiom is risky, an informative one is fatal. *) 
         (match flag_of_type env typ with
-           | (Info,_) -> axiom_error_message sp 
-           | (Logic,Arity) -> axiom_warning_message sp; 
+           | (Info,_) -> axiom_error_message kn 
+           | (Logic,Arity) -> axiom_warning_message kn; 
 	       DdummyType r
-	   | (Logic,_) -> axiom_warning_message sp;
+	   | (Logic,_) -> axiom_warning_message kn;
 	       Dterm (r, MLdummy'))
     | Some body ->
 	(match flag_of_type env typ with
@@ -676,20 +677,20 @@ let extract_constant sp r =
 	   | (Info, _) -> 
 		 let a = extract_term env body in
 		 if a <> MLdummy' then 
-		   Dterm (r, kill_prop_lams_eta a (signature_of_sp sp))
+		   Dterm (r, kill_prop_lams_eta a (signature_of_kn kn))
 		 else Dterm (r, a))
 		   
-let extract_constant_cache sp r = 
-  try lookup_constant sp 
+let extract_constant_cache kn r = 
+  try lookup_constant kn 
   with Not_found ->
-    let d = extract_constant sp r
-    in add_constant sp d; d
+    let d = extract_constant kn r
+    in add_constant kn d; d
 
 (*s From an inductive to a ML declaration. *)
       
-let extract_inductive_declaration sp =
-  extract_mib sp;
-  let ip = (sp,0) in 
+let extract_inductive_declaration kn =
+  extract_mib kn;
+  let ip = (kn,0) in 
   if is_singleton_inductive ip then
     let t = match lookup_constructor (ip,1) with 
       | Cml ([t],_,_)-> t
@@ -701,7 +702,7 @@ let extract_inductive_declaration sp =
      in 
     Dtype (IndRef ip,vl,t)
   else
-    let mib = Global.lookup_mind sp in
+    let mib = Global.lookup_mind kn in
     let one_ind ip n = 
       iterate_for (-n) (-1)
 	(fun j l -> 
@@ -713,7 +714,7 @@ let extract_inductive_declaration sp =
     let l = 
       iterate_for (1 - mib.mind_ntypes) 0
 	(fun i acc -> 
-	   let ip = (sp,-i) in
+	   let ip = (kn,-i) in
 	   let nc = Array.length mib.mind_packets.(-i).mind_consnames in 
 	   match lookup_inductive ip with
 	     | Iprop -> acc
@@ -725,9 +726,9 @@ let extract_inductive_declaration sp =
 (*s From a global reference to a ML declaration. *)
 
 let extract_declaration r = match r with
-  | ConstRef sp -> extract_constant sp r
-  | IndRef (sp,_) -> extract_inductive_declaration sp
-  | ConstructRef ((sp,_),_) -> extract_inductive_declaration sp
+  | ConstRef kn -> extract_constant kn r
+  | IndRef (kn,_) -> extract_inductive_declaration kn
+  | ConstructRef ((kn,_),_) -> extract_inductive_declaration kn
   | VarRef _ -> assert false
 
 (*s Check if a global reference corresponds to a logical inductive. *)
@@ -743,3 +744,4 @@ let decl_is_logical_ind = function
 let decl_is_singleton = function 
   | ConstructRef cp -> is_singleton_constructor cp 
   | _ -> false 
+
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index fe57be4272..0a273e7529 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -11,7 +11,8 @@
 (*s Extraction from Coq terms to Miniml. *)
 
 open Miniml
-open Nametab
+open Environ
+open Libnames
 
 (*s ML declaration corresponding to a Coq reference. *)
 
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index f87f11ed26..eb82e47521 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -13,7 +13,7 @@
 open Pp
 open Names
 open Term
-open Nametab
+open Libnames
 
 (*s ML type expressions. *)
 
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 544d8af6e3..5abd599ed0 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -18,7 +18,7 @@ open Miniml
 open Nametab
 open Table
 open Options
-open Nameops
+open Libnames
 (*i*)
 
 (*s Exceptions. *)
@@ -40,15 +40,15 @@ let id_of_name = function
 
 (*s Does a section path occur in a ML type ? *)
 
-let sp_of_r r = match r with 
-    | ConstRef sp -> sp
-    | IndRef (sp,_) -> sp
-    | ConstructRef ((sp,_),_) -> sp
+let kn_of_r r = match r with 
+    | ConstRef kn -> kn
+    | IndRef (kn,_) -> kn
+    | ConstructRef ((kn,_),_) -> kn
     | _ -> assert false
 
-let rec type_mem_sp sp = function 
-  | Tglob (r,l) -> (sp_of_r r) = sp || List.exists (type_mem_sp sp) l
-  | Tarr (a,b) -> (type_mem_sp sp a) || (type_mem_sp sp b)
+let rec type_mem_kn kn = function 
+  | Tglob (r,l) -> (kn_of_r r) = kn || List.exists (type_mem_kn kn) l
+  | Tarr (a,b) -> (type_mem_kn kn a) || (type_mem_kn kn b)
   | _ -> false
 
 (*S Generic functions over ML ast terms. *)
@@ -650,9 +650,9 @@ let is_ind = function
   | _ -> false 
 
 let is_rec_principle = function 
-  | ConstRef sp -> 
-      let d,i = repr_path sp in 
-      let s = string_of_id i in 
+  | ConstRef c -> 
+      let m,d,l = repr_kn c in 
+      let s = string_of_label l in 
       if Filename.check_suffix s "_rec" then 
 	let i' = id_of_string (Filename.chop_suffix s "_rec") in 
 	(try is_ind (locate (make_qualid d i'))
@@ -752,12 +752,13 @@ let inline_test t =
   not (is_fix t) && (is_constr t || (ml_size t < 12 && is_not_strict t))
 
 let manual_inline_list = 
-  List.map (fun s -> path_of_string ("Coq.Init."^s))
-    [ (* "Wf.Acc_rec" ; "Wf.Acc_rect" ; *)
-      "Wf.well_founded_induction" ; "Wf.well_founded_induction_type" ]
+  let dir =  dirpath_of_string "Coq.Init.Wf" 
+  in List.map (fun s -> encode_kn dir (id_of_string s))
+       [ "Acc_rec" ; "Acc_rect" ; 
+	 "well_founded_induction" ; "well_founded_induction_type" ]
 
 let manual_inline = function 
-  | ConstRef sp -> List.mem sp manual_inline_list
+  | ConstRef c -> List.mem c manual_inline_list
   | _ -> false 
 
 (* If the user doesn't say he wants to keep [t], we inline in two cases:
@@ -838,7 +839,7 @@ and optimize_Dfix prm r t b l =
 	  else optimize prm l
 	else 
 	  let v = try 
-	    let d = dirpath (sp_of_r r) in 
+	    let d,_ = decode_kn (kn_of_r r) in 
 	    Array.map (fun id -> locate (make_qualid d id)) f 
 	  with Not_found -> raise Impossible 
 	  in 
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index 778c7ee51e..854e3b5e47 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -10,7 +10,7 @@
 
 open Names
 open Term
-open Nametab
+open Libnames
 open Miniml
 
 
@@ -41,9 +41,9 @@ val named_lams : identifier list -> ml_ast -> ml_ast
 (*s Utility functions over ML types. [update_args sp vl t] puts [vl]
    as arguments behind every inductive types [(sp,_)]. *)
 
-val sp_of_r : global_reference -> section_path
+val kn_of_r : global_reference -> kernel_name
 
-val type_mem_sp : section_path -> ml_type -> bool
+val type_mem_kn : kernel_name -> ml_type -> bool
 
 (*s Utility functions over ML terms. [occurs n t] checks whether [Rel
     n] occurs (freely) in [t]. [ml_lift] is de Bruijn
@@ -55,6 +55,8 @@ val occurs : int -> ml_ast -> bool
 
 val ml_lift : int -> ml_ast -> ml_ast
 
+val ml_subst : ml_ast -> ml_ast -> ml_ast
+
 val ml_pop : ml_ast -> ml_ast
 
 (*s Some transformations of ML terms. [optimize] simplify
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 34b57a45c1..af1a9c2265 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -19,7 +19,7 @@ open Util
 open Pp
 open Term 
 open Declarations
-open Nametab
+open Libnames
 open Reduction
 
 (*s AutoInline parameter *)
@@ -77,11 +77,11 @@ let lang_ref = ref Ocaml
 let lang () = !lang_ref
 
 let (extr_lang,_) = 
-  declare_object ("Extraction Lang", 
-		  {cache_function = (fun (_,l) -> lang_ref := l);
-		   load_function = (fun (_,l) -> lang_ref := l);
-		   open_function = (fun _ -> ());
-		   export_function = (fun x -> Some x) })
+  declare_object 
+    {(default_object "Extraction Lang") with  
+       cache_function = (fun (_,l) -> lang_ref := l);
+       load_function = (fun _ (_,l) -> lang_ref := l);
+       export_function = (fun x -> Some x)}
 
 let _ = declare_summary "Extraction Lang" 
 	  { freeze_function = (fun () -> !lang_ref);
@@ -111,11 +111,11 @@ let add_inline_entries b l =
 (*s Registration of operations for rollback. *)
 
 let (inline_extraction,_) = 
-  declare_object ("Extraction Inline",
-		  { cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
-		    load_function = (fun (_,(b,l)) -> add_inline_entries b l);
-		    open_function = (fun _ -> ());
-		    export_function = (fun x -> Some x) })
+  declare_object 
+    {(default_object "Extraction Inline") with 
+       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)}
 
 let _ = declare_summary "Extraction Inline"
 	  { freeze_function = (fun () -> !inline_table);
@@ -148,11 +148,10 @@ let print_extraction_inline () =
 
 let (reset_inline,_) = 
   declare_object
-    ("Reset Extraction Inline", 
-     {  cache_function = (fun (_,_)-> inline_table :=  empty_inline_table);
-	load_function = (fun (_,_)-> inline_table :=  empty_inline_table); 
-	open_function = (fun _ -> ());
-	export_function = (fun x -> Some x) })
+    {(default_object "Reset Extraction Inline") with  
+       cache_function = (fun (_,_)-> inline_table :=  empty_inline_table);
+       load_function = (fun _ (_,_)-> inline_table :=  empty_inline_table); 
+       export_function = (fun x -> Some x)}
 
 let reset_extraction_inline () = add_anonymous_leaf (reset_inline ())
 
@@ -199,12 +198,11 @@ let find_ml_extraction r = snd (Refmap.find r (fst !extractions))
 
 let (in_ml_extraction,_) = 
   declare_object 
-    ("ML extractions",
-     { cache_function = (fun (_,(r,k,s)) -> add_ml_extraction r k s);
-       load_function = (fun (_,(r,k,s)) -> add_ml_extraction r k s);
-       open_function = (fun _ -> ());
-       export_function = (fun x -> Some x) })
-    
+    {(default_object "ML extractions") with 
+       cache_function = (fun (_,(r,k,s)) -> add_ml_extraction r k s);
+       load_function = (fun _ (_,(r,k,s)) -> add_ml_extraction r k s);
+       export_function = (fun x -> Some x)}
+
 let _ = declare_summary "ML extractions"
 	  { freeze_function = (fun () -> !extractions);
 	    unfreeze_function = ((:=) extractions);
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 1e21e494b9..063c18a3c7 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -10,7 +10,7 @@
 
 open Vernacinterp
 open Names
-open Nametab
+open Libnames
 
 (*s AutoInline parameter *) 
 
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 7dc6d961fa..d5c50f9d34 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -34,7 +34,7 @@ let constant dir s =
     Declare.global_reference_in_absolute_module dir id
   with Not_found ->
     anomaly ("Field: cannot find "^
-	     (Nametab.string_of_qualid (Nametab.make_qualid dir id)))
+	     (Libnames.string_of_qualid (Libnames.make_qualid dir id)))
 
 (* To deal with the optional arguments *)
 let constr_of_opt a opt =
@@ -44,12 +44,12 @@ let constr_of_opt a opt =
   | Some f -> mkApp ((constant ["Field_Compl"] "Some"),[|ac;constr_of f|])
 
 (* Table of theories *)
-let th_tab = ref ((Hashtbl.create 53) : (constr,constr) Hashtbl.t)
+let th_tab = ref (Gmap.empty : (constr,constr) Gmap.t)
 
-let lookup typ = Hashtbl.find !th_tab typ
+let lookup typ = Gmap.find typ !th_tab
 
 let _ = 
-  let init () = th_tab := (Hashtbl.create 53) in
+  let init () = th_tab := Gmap.empty in
   let freeze () = !th_tab in
   let unfreeze fs = th_tab := fs in
   Summary.declare_summary "field"
@@ -59,17 +59,22 @@ let _ =
       Summary.survive_section   = false }
 
 let load_addfield _ = ()
-let cache_addfield (_,(typ,th)) = Hashtbl.add !th_tab typ th
+let cache_addfield (_,(typ,th)) = th_tab := Gmap.add typ th !th_tab
+let subst_addfield (_,subst,(typ,th as obj)) =
+  let typ' = subst_mps subst typ in
+  let th' = subst_mps subst th in
+    if typ' == typ && th' == th then obj else
+      (typ',th')
 let export_addfield x = Some x
 
 (* Declaration of the Add Field library object *)
 let (in_addfield,out_addfield)=
-  Libobject.declare_object
-    ("ADD_FIELD",
-     { Libobject.load_function = load_addfield;
-       Libobject.open_function = cache_addfield;
+  Libobject.declare_object {(Libobject.default_object "ADD_FIELD") with
+       Libobject.open_function = (fun i o -> if i=1 then cache_addfield o);
        Libobject.cache_function = cache_addfield;
-       Libobject.export_function = export_addfield })
+       Libobject.subst_function = subst_addfield;
+       Libobject.classify_function = (fun (_,a) -> Libobject.Substitute a);
+       Libobject.export_function = export_addfield }
 
 (* Adds a theory to the table *)
 let add_field a aplus amult aone azero aopp aeq ainv aminus_o adiv_o rth
@@ -128,7 +133,7 @@ END
 
 (* Guesses the type and calls Field_Gen with the right theory *)
 let field g =
-  Library.check_required_module ["Coq";"field";"Field"];
+  Library.check_required_library ["Coq";"field";"Field"];
   let evc = project g
   and env = pf_env g in
   let ist = { evc=evc; env=env; lfun=[]; lmatch=[];
@@ -162,7 +167,7 @@ let guess_theory env evc = function
 
 (* Guesses the type and calls Field_Term with the right theory *)
 let field_term l g =
-  Library.check_required_module ["Coq";"field";"Field"];
+  Library.check_required_library ["Coq";"field";"Field"];
   let env = (pf_env g)
   and evc = (project g) in
   let th = valueIn (VConstr (guess_theory env evc l))
diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml
index 2cdb929ae5..aac632de98 100644
--- a/contrib/fourier/fourierR.ml
+++ b/contrib/fourier/fourierR.ml
@@ -18,6 +18,7 @@ open Term
 open Tactics
 open Clenv
 open Names
+open Libnames
 open Tacticals
 open Tacmach
 open Fourier
@@ -76,43 +77,46 @@ let parse s = Astterm.interp_constr Evd.empty (Global.env()) (parse_ast s);;
 let pf_parse_constr gl s =
    Astterm.interp_constr Evd.empty (pf_env gl) (parse_ast s);;
 
-let rec string_of_constr c =
+let string_of_R_constant kn = 
+  match Names.repr_kn kn with
+    | MPfile dir, sec_dir, id when 
+	sec_dir = empty_dirpath && 
+	string_of_dirpath dir = "Coq.Reals.Rdefinitions" 
+	-> string_of_label id
+    | _ -> "constant_not_of_R"
+
+let rec string_of_R_constr c =
  match kind_of_term c with
-   Cast (c,t) -> string_of_constr c
-  |Const c -> string_of_path c
-  |Var(c) -> string_of_id c
+   Cast (c,t) -> string_of_R_constr c
+  |Const c -> string_of_R_constant c
   | _ -> "not_of_constant"
-;;
 
 let rec rational_of_constr c =
   match kind_of_term c with
   | Cast (c,t) -> (rational_of_constr c)
   | App (c,args) ->
-        (match kind_of_term c with
-           Const c ->
-               (match (string_of_path c) with
-		 "Coq.Reals.Rdefinitions.Ropp" -> 
-		      rop (rational_of_constr args.(0))
-		|"Coq.Reals.Rdefinitions.Rinv" -> 
-                      rinv (rational_of_constr args.(0))
-                |"Coq.Reals.Rdefinitions.Rmult" -> 
-                      rmult (rational_of_constr args.(0))
-                            (rational_of_constr args.(1))
-                |"Coq.Reals.Rdefinitions.Rdiv" -> 
-                      rdiv (rational_of_constr args.(0))
-                            (rational_of_constr args.(1))
-                |"Coq.Reals.Rdefinitions.Rplus" -> 
-                      rplus (rational_of_constr args.(0))
-                            (rational_of_constr args.(1))
-                |"Coq.Reals.Rdefinitions.Rminus" -> 
-                      rminus (rational_of_constr args.(0))
-                             (rational_of_constr args.(1))
-                | _ -> failwith "not a rational")
-          | _ -> failwith "not a rational")
-  | Const c ->
-        (match (string_of_path c) with
-	       "Coq.Reals.Rdefinitions.R1" -> r1
-              |"Coq.Reals.Rdefinitions.R0" -> r0
+      (match (string_of_R_constr c) with
+	 | "Ropp" -> 
+	     rop (rational_of_constr args.(0))
+	 | "Rinv" -> 
+	     rinv (rational_of_constr args.(0))
+	 | "Rmult" -> 
+	     rmult (rational_of_constr args.(0))
+                   (rational_of_constr args.(1))
+	 | "Rdiv" -> 
+	     rdiv (rational_of_constr args.(0))
+                  (rational_of_constr args.(1))
+	 | "Rplus" -> 
+	     rplus (rational_of_constr args.(0))
+                   (rational_of_constr args.(1))
+	 | "Rminus" -> 
+	     rminus (rational_of_constr args.(0))
+                    (rational_of_constr args.(1))
+	 | _ -> failwith "not a rational")
+  | Const kn ->
+      (match (string_of_R_constant kn) with
+	       "R1" -> r1
+              |"R0" -> r0
               |  _ -> failwith "not a rational")
   |  _ -> failwith "not a rational"
 ;;
@@ -122,43 +126,40 @@ let rec flin_of_constr c =
     match kind_of_term c with
   | Cast (c,t) -> (flin_of_constr c)
   | App (c,args) ->
-        (match kind_of_term c with
-           Const c ->
-            (match (string_of_path c) with
-	     "Coq.Reals.Rdefinitions.Ropp" -> 
-                  flin_emult (rop r1) (flin_of_constr args.(0))
-	    |"Coq.Reals.Rdefinitions.Rplus"-> 
-                  flin_plus (flin_of_constr args.(0))
-	                    (flin_of_constr args.(1))
-	    |"Coq.Reals.Rdefinitions.Rminus"->
-                  flin_minus (flin_of_constr args.(0))
-	                     (flin_of_constr args.(1))
-	    |"Coq.Reals.Rdefinitions.Rmult"->
+      (match (string_of_R_constr c) with
+	   "Ropp" -> 
+             flin_emult (rop r1) (flin_of_constr args.(0))
+	 | "Rplus"-> 
+             flin_plus (flin_of_constr args.(0))
+	               (flin_of_constr args.(1))
+	 | "Rminus"->
+             flin_minus (flin_of_constr args.(0))
+	                (flin_of_constr args.(1))
+	 | "Rmult"->
 	     (try (let a=(rational_of_constr args.(0)) in
-                   try (let b = (rational_of_constr args.(1)) in
+                     try (let b = (rational_of_constr args.(1)) in
 			    (flin_add_cste (flin_zero()) (rmult a b)))
-		   with _-> (flin_add (flin_zero())
-		             args.(1) 
-                             a))
+		     with _-> (flin_add (flin_zero())
+				 args.(1) 
+				 a))
 	      with _-> (flin_add (flin_zero())
-				 args.(0) 
-				 (rational_of_constr args.(1))))
-	    |"Coq.Reals.Rdefinitions.Rinv"->
-	       let a=(rational_of_constr args.(0)) in
+			  args.(0) 
+			  (rational_of_constr args.(1))))
+	 | "Rinv"->
+	     let a=(rational_of_constr args.(0)) in
 	       flin_add_cste (flin_zero()) (rinv a)
-	    |"Coq.Reals.Rdefinitions.Rdiv"->
-	      (let b=(rational_of_constr args.(1)) in
-	       try (let a = (rational_of_constr args.(0)) in
+	 | "Rdiv"->
+	     (let b=(rational_of_constr args.(1)) in
+		try (let a = (rational_of_constr args.(0)) in
 		       (flin_add_cste (flin_zero()) (rdiv a b)))
-	       with _-> (flin_add (flin_zero())
-		             args.(0) 
-                             (rinv b)))
-            |_->assert false)
-           |_ -> assert false)
+		with _-> (flin_add (flin_zero())
+		            args.(0) 
+                            (rinv b)))
+         |_->assert false)
   | Const c ->
-        (match (string_of_path c) with
-	       "Coq.Reals.Rdefinitions.R1" -> flin_one ()
-              |"Coq.Reals.Rdefinitions.R0" -> flin_zero ()
+        (match (string_of_R_constant c) with
+	       "R1" -> flin_one ()
+              |"R0" -> flin_zero ()
               |_-> assert false)
   |_-> assert false)
   with _ -> flin_add (flin_zero())
@@ -191,29 +192,29 @@ let ineq1_of_constr (h,t) =
          let t2= args.(1) in
          (match kind_of_term f with
            Const c ->
-            (match (string_of_path c) with
-		 "Coq.Reals.Rdefinitions.Rlt" -> [{hname=h;
+            (match (string_of_R_constant c) with
+		 "Rlt" -> [{hname=h;
                            htype="Rlt";
 		           hleft=t1;
 			   hright=t2;
 			   hflin= flin_minus (flin_of_constr t1)
                                              (flin_of_constr t2);
 			   hstrict=true}]
-		|"Coq.Reals.Rdefinitions.Rgt" -> [{hname=h;
+		|"Rgt" -> [{hname=h;
                            htype="Rgt";
 		           hleft=t2;
 			   hright=t1;
 			   hflin= flin_minus (flin_of_constr t2)
                                              (flin_of_constr t1);
 			   hstrict=true}]
-		|"Coq.Reals.Rdefinitions.Rle" -> [{hname=h;
+		|"Rle" -> [{hname=h;
                            htype="Rle";
 		           hleft=t1;
 			   hright=t2;
 			   hflin= flin_minus (flin_of_constr t1)
                                              (flin_of_constr t2);
 			   hstrict=false}]
-		|"Coq.Reals.Rdefinitions.Rge" -> [{hname=h;
+		|"Rge" -> [{hname=h;
                            htype="Rge";
 		           hleft=t2;
 			   hright=t1;
@@ -221,15 +222,15 @@ let ineq1_of_constr (h,t) =
                                              (flin_of_constr t1);
 			   hstrict=false}]
                 |_->assert false)
-          | Ind (sp,i) ->
-              (match (string_of_path sp) with 
-		 "Coq.Init.Logic_Type.eqT" ->  let t0= args.(0) in
+          | Ind (kn,i) ->
+	      if IndRef(kn,i) = Coqlib.glob_eqT then
+		           let t0= args.(0) in
                            let t1= args.(1) in
                            let t2= args.(2) in
 		    (match (kind_of_term t0) with
                          Const c ->
-			   (match (string_of_path c) with
-			      "Coq.Reals.Rdefinitions.R"->
+			   (match (string_of_R_constant c) with
+			      "R"->
                          [{hname=h;
                            htype="eqTLR";
 		           hleft=t1;
@@ -246,7 +247,8 @@ let ineq1_of_constr (h,t) =
 			   hstrict=false}]
                            |_-> assert false)
                          |_-> assert false)
-                   |_-> assert false)
+	      else
+		assert false
           |_-> assert false)
         |_-> assert false
 ;;
@@ -373,17 +375,17 @@ let tac_use h = match h.htype with
 
 let is_ineq (h,t) =
     match (kind_of_term t) with
-       App (f,args) ->
-         (match (string_of_constr f) with
-		 "Coq.Reals.Rdefinitions.Rlt" -> true
-		|"Coq.Reals.Rdefinitions.Rgt" -> true
-		|"Coq.Reals.Rdefinitions.Rle" -> true
-		|"Coq.Reals.Rdefinitions.Rge" -> true
-		|"Coq.Init.Logic_Type.eqT" -> (match (string_of_constr args.(0)) with
-                            "Coq.Reals.Rdefinitions.R"->true
-			    |_->false)
-                |_->false)
-     |_->false
+	App (f,args) ->
+	  (match (string_of_R_constr f) with
+	       "Rlt" -> true
+	     | "Rgt" -> true
+	     | "Rle" -> true
+	     | "Rge" -> true
+	     | "eqT" -> (match (string_of_R_constr args.(0)) with
+			     "R" -> true
+			   | _ -> false)
+             | _ ->false)
+      |_->false
 ;;
 
 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
@@ -395,7 +397,7 @@ let mkAppL a =
 
 (* Résolution d'inéquations linéaires dans R *)
 let rec fourier gl=
-    Library.check_required_module ["Coq";"fourier";"Fourier"];
+    Library.check_required_library ["Coq";"fourier";"Fourier"];
     let parse = pf_parse_constr gl in
     let goal = strip_outer_cast (pf_concl gl) in
     let fhyp=id_of_string "new_hyp_for_fourier" in
@@ -404,23 +406,23 @@ let rec fourier gl=
     try (let tac =
      match (kind_of_term goal) with
       App (f,args) ->
-      (match (string_of_constr f) with
-	     "Coq.Reals.Rdefinitions.Rlt" -> 
+      (match (string_of_R_constr f) with
+	     "Rlt" -> 
 	       (tclTHEN
 	         (tclTHEN (apply (parse "Rfourier_not_ge_lt"))
 			  (intro_using  fhyp))
 		 fourier)
-	    |"Coq.Reals.Rdefinitions.Rle" -> 
+	    |"Rle" -> 
 	     (tclTHEN
 	      (tclTHEN (apply (parse "Rfourier_not_gt_le"))
 		       (intro_using  fhyp))
 			fourier)
-	    |"Coq.Reals.Rdefinitions.Rgt" -> 
+	    |"Rgt" -> 
 	     (tclTHEN
 	      (tclTHEN (apply (parse "Rfourier_not_le_gt"))
 		       (intro_using  fhyp))
 	      fourier)
-	    |"Coq.Reals.Rdefinitions.Rge" -> 
+	    |"Rge" -> 
 	     (tclTHEN
 	      (tclTHEN (apply (parse "Rfourier_not_lt_ge"))
 		       (intro_using  fhyp))
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index 92f6f285f8..a0620d4ba2 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -7,6 +7,7 @@ open Util;;
 open Ast;;
 open Term;;
 open Pp;;
+open Libnames;;
 open Libobject;;
 open Library;;
 open Vernacinterp;;
@@ -258,9 +259,8 @@ let filter_by_module_from_varg_list l =
 
 let add_search (global_reference:global_reference) assumptions cstr =
   try 
-    let env = Global.env() in
   let id_string =
-    string_of_qualid (Nametab.shortest_qualid_of_global env 
+    string_of_qualid (Nametab.shortest_qualid_of_global None 
 			global_reference) in
   let ast = 
     try
@@ -321,15 +321,13 @@ and ntyp = nf_betaiota typ in
 
 (* The following function is copied from globpr in env/printer.ml *)
 let globcv x =
-  let env = Global.env() in 
     match x with
       | Node(_,"MUTIND", (Path(_,sp))::(Num(_,tyi))::_) ->
-	  let env = Global.env() in
 	    convert_qualid
-	      (Nametab.shortest_qualid_of_global env (IndRef(sp,tyi)))
+	      (Nametab.shortest_qualid_of_global None (IndRef(sp,tyi)))
       | Node(_,"MUTCONSTRUCT",(Path(_,sp))::(Num(_,tyi))::(Num(_,i))::_) ->
 	  convert_qualid
-            (Nametab.shortest_qualid_of_global env
+            (Nametab.shortest_qualid_of_global None
 	       (ConstructRef ((sp, tyi), i)))
   | _ -> failwith "globcv : unexpected value";;
 
@@ -412,20 +410,20 @@ let inspect n =
       (fun a ->
 	 try
            (match a with
-             	sp, Lib.Leaf lobj ->
-		  (match sp, object_tag lobj with
-                       _, "VARIABLE" ->
+             	oname, Lib.Leaf lobj ->
+		  (match oname, object_tag lobj with
+                       (sp,_), "VARIABLE" ->
 			 let ((_, _, v), _) = get_variable (basename sp) in
 			   add_search2 (Nametab.locate (qualid_of_sp sp)) v
-		     | sp, ("CONSTANT"|"PARAMETER") ->
-			 let {const_type=typ} = Global.lookup_constant sp in
+		     | (sp,kn), ("CONSTANT"|"PARAMETER") ->
+			 let {const_type=typ} = Global.lookup_constant kn in
 			   add_search2 (Nametab.locate (qualid_of_sp sp)) typ
-		     | sp, "MUTUALINDUCTIVE" ->
+		     | (sp,kn), "MUTUALINDUCTIVE" ->
 			 add_search2 (Nametab.locate (qualid_of_sp sp))
 			   (Pretyping.understand Evd.empty (Global.env())
-			      (RRef(dummy_loc, IndRef(sp,0))))
+			      (RRef(dummy_loc, IndRef(kn,0))))
 		     | _ -> failwith ("unexpected value 1 for "^ 
-				      (string_of_id (basename sp))))
+				      (string_of_id (basename (fst oname)))))
               | _ -> failwith "unexpected value")
 	 with e -> ())
       l;
diff --git a/contrib/interface/ctast.ml b/contrib/interface/ctast.ml
index c5611f985a..2345ff4719 100644
--- a/contrib/interface/ctast.ml
+++ b/contrib/interface/ctast.ml
@@ -1,6 +1,7 @@
 (* A copy of pre V7 ast *)
 
 open Names
+open Libnames
 
 type loc = int * int
 
@@ -17,7 +18,7 @@ type t =
 let section_path sl =
   match List.rev sl with
     | s::pa ->
-	make_path
+	Libnames.encode_kn
 	  (make_dirpath (List.map id_of_string pa))
 	  (id_of_string s)
     | [] -> invalid_arg "section_path"
@@ -55,7 +56,7 @@ let rec ast_to_ct = function
   | Coqast.Id (loc,a) -> Id (loc,a)
   | Coqast.Str (loc,a) -> Str (loc,a)
   | Coqast.Path (loc,a) ->
-    let (sl,bn) = repr_path a in
+    let (sl,bn) = Libnames.decode_kn a in
     Path(loc, (List.map string_of_id
                 (List.rev (repr_dirpath sl))) @ [string_of_id bn])
   | Coqast.Dynamic (loc,a) -> Dynamic (loc,a)
diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml
index 9d90782e4d..3be5d8a36a 100644
--- a/contrib/interface/dad.ml
+++ b/contrib/interface/dad.ml
@@ -15,6 +15,7 @@ open Ctast;;
 open Termast;;
 open Astterm;;
 open Vernacinterp;;
+open Libnames;;
 open Nametab
 
 open Proof_type;;
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 8c6293ae2c..79375cf2b3 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -8,6 +8,7 @@ open Termast;;
 open Term;;
 open Impargs;;
 open Reduction;;
+open Libnames;;
 open Libobject;;
 open Environ;;
 open Declarations;;
@@ -83,7 +84,7 @@ let implicit_args_to_ast_list sp mipv =
 	| _ -> [VernacComments (List.rev implicit_args_descriptions)];;
 	      
 let convert_qualid qid =
-  let d, id = Nametab.repr_qualid qid in
+  let d, id = Libnames.repr_qualid qid in
     match repr_dirpath d with
 	[] -> nvar id
       | d -> ope("QUALID", List.fold_left (fun l s -> (nvar s)::l)
@@ -108,7 +109,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 env (IndRef (sp, tyi)) in
+  let sp = sp_of_global None (IndRef (sp, tyi)) in
   (basename sp,
    convert_env(List.rev params),
    (ast_of_constr true envpar arity),
@@ -167,16 +168,16 @@ let make_definition_ast name c typ implicits =
   ::(implicits_to_ast_list implicits);;
 
 (* This function is inspired by print_constant *)
-let constant_to_ast_list sp =
-  let cb = Global.lookup_constant sp in
+let constant_to_ast_list kn =
+  let cb = Global.lookup_constant kn in
   let c = cb.const_body in
   let typ = cb.const_type in
-  let l = constant_implicits_list sp in
+  let l = constant_implicits_list kn in
   (match c with
       None -> 
-	make_variable_ast (basename sp) typ l
+	make_variable_ast (id_of_label (label kn)) typ l
     | Some c1 ->
-	make_definition_ast (basename sp) c1 typ l)
+	make_definition_ast (id_of_label (label kn)) c1 typ l)
 
 let variable_to_ast_list sp =
   let ((id, c, v), _) = get_variable sp in
@@ -195,13 +196,13 @@ let inductive_to_ast_list sp =
 
 (* this function is inspired by print_leaf_entry from pretty.ml *)
 
-let leaf_entry_to_ast_list (sp,lobj) =
+let leaf_entry_to_ast_list ((sp,kn),lobj) =
   let tag = object_tag lobj in
-  match (sp,tag) with
-  | (_, "VARIABLE") -> variable_to_ast_list (basename sp)
-  | (_, ("CONSTANT"|"PARAMETER")) -> constant_to_ast_list sp
-  | (_, "INDUCTIVE") -> inductive_to_ast_list sp
-  | (_, s) -> 
+  match tag with
+  | "VARIABLE" -> variable_to_ast_list (basename sp)
+  | "CONSTANT"|"PARAMETER" -> constant_to_ast_list kn
+  | "INDUCTIVE" -> inductive_to_ast_list kn
+  | s -> 
       errorlabstrm 
       	"print" (str ("printing of unrecognized object " ^
 		      s ^ " has been required"));;
@@ -210,13 +211,13 @@ let leaf_entry_to_ast_list (sp,lobj) =
 
 
 (* this function is inspired by print_name *)
-let name_to_ast (qid:Nametab.qualid) = 
+let name_to_ast qid = 
   let l = 
     try
       let sp = Nametab.locate_obj qid in
       let (sp,lobj) = 
       	let (sp,entry) =
-          List.find (fun en -> (fst en) = sp) (Lib.contents_after None)
+          List.find (fun en -> (fst (fst en)) = sp) (Lib.contents_after None)
       	in
 	  match entry with
             | Lib.Leaf obj -> (sp,obj)
@@ -232,7 +233,7 @@ let name_to_ast (qid:Nametab.qualid) =
 	  | VarRef sp -> variable_to_ast_list sp
   	with Not_found -> 
 	  try  (* Var locale de but, pas var de section... donc pas d'implicits *)
-	    let dir,name = Nametab.repr_qualid qid in 
+	    let dir,name = repr_qualid qid in 
 	      if (repr_dirpath dir) <> [] then raise Not_found;
 	      let (_,c,typ) = Global.lookup_named name in 
 		(match c with
@@ -240,12 +241,12 @@ let name_to_ast (qid:Nametab.qualid) =
 		   | Some c1 -> make_definition_ast name c1 typ [])
 	  with Not_found ->
 	    try
-	      let sp = Syntax_def.locate_syntactic_definition qid in
+	      let sp = Nametab.locate_syntactic_definition qid in
 		errorlabstrm "print"
       		  (str "printing of syntax definitions not implemented")
 	    with Not_found ->
 	      errorlabstrm "print"
-		(Nametab.pr_qualid qid ++
+		(pr_qualid qid ++
 		 spc () ++ str "not a defined object")
   in
   VernacList (List.map (fun x -> (dummy_loc,x)) l)
diff --git a/contrib/interface/name_to_ast.mli b/contrib/interface/name_to_ast.mli
index 4a68e0134f..600ec5f918 100644
--- a/contrib/interface/name_to_ast.mli
+++ b/contrib/interface/name_to_ast.mli
@@ -1,2 +1,2 @@
-val name_to_ast : Nametab.qualid -> Vernacexpr.vernac_expr;;
-val convert_qualid : Nametab.qualid -> Coqast.t;;
+val name_to_ast : Libnames.qualid -> Vernacexpr.vernac_expr;;
+val convert_qualid : Libnames.qualid -> Coqast.t;;
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index 5bce60f223..61fd060724 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -6,6 +6,8 @@ open Ctast;;
 
 open Pp;;
 
+open Libnames;;
+
 open Library;;
 
 open Ascent;;
@@ -67,7 +69,7 @@ let try_require_module import specif names =
     else Some (specif = "SPECIFICATION"))
    (List.map 
      (fun name ->
-       (dummy_loc,Nametab.make_short_qualid (Names.id_of_string name)))
+       (dummy_loc,Libnames.make_short_qualid (Names.id_of_string name)))
       names)
    (import = "IMPORT")
  with
@@ -110,7 +112,7 @@ let execute_when_necessary v =
       (try 
 	Vernacentries.interp v
        with _ ->
-	 let l=prlist_with_sep spc (fun (_,qid) -> Nametab.pr_qualid qid) l in
+	 let l=prlist_with_sep spc (fun (_,qid) -> pr_qualid qid) l in
 	 msgnl (str "Reinterning of " ++ l ++ str " failed"))
   | VernacRequireFrom (_,_,name,_) ->
       (try 
@@ -427,10 +429,10 @@ let print_version_action () =
 let load_syntax_action reqid module_name =
  msg (str "loading " ++ str module_name ++ str "... ");
  try
-      (let qid = Nametab.make_short_qualid (Names.id_of_string module_name) in
-      read_module (dummy_loc,qid);
+      (let qid = Libnames.make_short_qualid (Names.id_of_string module_name) in
+      read_library (dummy_loc,qid);
       msg (str "opening... ");
-      import_module false (dummy_loc,qid); 
+      Declaremods.import_module (Nametab.locate_module qid); 
       msgnl (str "done" ++ fnl ());
       ())
  with
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index 5dd9d071b5..55aae90be2 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -29,7 +29,7 @@ let get_hyp_by_name g name =
        ("hyp",judgment.uj_type))
 (* je sais, c'est pas beau, mais je ne sais pas trop me servir de look_up...
    Loïc *)
-  with _ -> (let ast = Termast.ast_of_qualid (Nametab.make_short_qualid name)in
+  with _ -> (let ast = Termast.ast_of_qualid (Libnames.make_short_qualid name)in
              let c = Astterm.interp_constr evd env ast in
              ("cste",type_of (Global.env()) Evd.empty c))
 ;;
@@ -252,7 +252,7 @@ let reference dir s =
     Nametab.locate_in_absolute_module dir id
   with Not_found ->
     anomaly ("Coqlib: cannot find "^
-	     (Nametab.string_of_qualid (Nametab.make_qualid dir id)))
+	     (Libnames.string_of_qualid (Libnames.make_qualid dir id)))
 
 let constant dir s =  Declare.constr_of_reference (reference dir s);;
 
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index ae876e129f..c7e6be1318 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -6,6 +6,7 @@ open Environ
 open Evd
 open Names
 open Nameops
+open Libnames
 open Term
 open Termops
 open Util
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index d1af58df70..a2620c67f7 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -344,9 +344,9 @@ let qualid_to_ct_ID =
     | Node(_, "QUALIDMETA",[Num(_,n)]) -> Some(CT_metac (CT_int n))
     | _ -> None;;
 
-let tac_qualid_to_ct_ID qid = CT_ident (Nametab.string_of_qualid qid)
+let tac_qualid_to_ct_ID qid = CT_ident (Libnames.string_of_qualid qid)
 
-let loc_qualid_to_ct_ID (_,qid) = CT_ident (Nametab.string_of_qualid qid)
+let loc_qualid_to_ct_ID (_,qid) = CT_ident (Libnames.string_of_qualid qid)
 
 let qualid_or_meta_to_ct_ID = function
   | AN (_,qid) -> tac_qualid_to_ct_ID qid
@@ -360,7 +360,7 @@ let xlate_qualid_list l = CT_id_list (List.map loc_qualid_to_ct_ID l)
 
 let reference_to_ct_ID = function
   | RIdent (_,id) -> CT_ident (Names.string_of_id id)
-  | RQualid (_,qid) -> CT_ident (Nametab.string_of_qualid qid)
+  | RQualid (_,qid) -> CT_ident (Libnames.string_of_qualid qid)
 
 let xlate_class = function
   | FunClass -> CT_ident "FUNCLASS"
@@ -437,10 +437,10 @@ let xlate_op the_node opn a b =
   (match a, b with
   | ((Path (_, sl)) :: []), [] ->
     CT_coerce_ID_to_FORMULA(CT_ident
-       (Names.string_of_id (Nameops.basename (section_path sl))))
+       (Names.string_of_label (Names.label (section_path sl))))
   | ((Path (_, sl)) :: []), tl ->
  CT_coerce_ID_to_FORMULA(CT_ident   
-       (Names.string_of_id(Nameops.basename (section_path sl))))
+       (Names.string_of_label(Names.label (section_path sl))))
   | _, _ -> xlate_error "xlate_op : CONST")
  | (** string_of_path needs to be investigated.
     *)
@@ -454,8 +454,8 @@ let xlate_op the_node opn a b =
 		  | _ -> assert false
 	    else
 	    CT_coerce_ID_to_FORMULA(
-	      CT_ident(Names.string_of_id
-			 (Nameops.basename (section_path sl))))
+	      CT_ident(Names.string_of_label
+			 (Names.label (section_path sl))))
   	| _, _ -> xlate_error "xlate_op : MUTIND")
  | "CASE"
  | "MATCH" ->
@@ -478,7 +478,10 @@ let xlate_op the_node opn a b =
 	 | Some(Rform x) -> x
 	 | _ -> assert false
    else
-   let name = Names.string_of_path (section_path sl) in
+   let name = 
+     let dir,id = Libnames.decode_kn (section_path sl) in
+       Names.string_of_dirpath (Libnames.extend_dirpath dir id) 
+   in
      (* This is rather a patch to cope with the fact that identifier
         names have disappeared from the vo files for grammar rules *)
        let type_desc = (try Some (Hashtbl.find type_table name) with
@@ -2864,7 +2867,7 @@ let xlate_vernac =
 (*
      | "EndSection", ((Varg_ident id) :: []) ->
 *)
-  | VernacEndSection id -> CT_section_end (xlate_ident id)
+  | VernacEndSegment id -> CT_section_end (xlate_ident id)
 (*
      | "StartProof",
          ((Varg_string (CT_string kind)) :: ((Varg_ident s) :: (c :: []))) ->
@@ -3249,9 +3252,9 @@ let xlate_vernac =
       let local_opt =
        match s with
        (* Cannot decide whether it is a global or a Local but at toplevel *)
-       | Nametab.NeverDischarge -> CT_coerce_NONE_to_LOCAL_OPT CT_none
-       | Nametab.DischargeAt _ -> CT_local
-       | Nametab.NotDeclare -> assert false in
+       | Libnames.NeverDischarge -> CT_coerce_NONE_to_LOCAL_OPT CT_none
+       | Libnames.DischargeAt _ -> CT_local
+       | Libnames.NotDeclare -> assert false in
       CT_coercion (local_opt, id_opt, loc_qualid_to_ct_ID id1,
         xlate_class id2, xlate_class id3)
 
@@ -3260,9 +3263,9 @@ let xlate_vernac =
       let local_opt =
        match s with
        (* Cannot decide whether it is a global or a Local but at toplevel *)
-       | Nametab.NeverDischarge -> CT_coerce_NONE_to_LOCAL_OPT CT_none
-       | Nametab.DischargeAt _ -> CT_local 
-       | Nametab.NotDeclare -> assert false in
+       | Libnames.NeverDischarge -> CT_coerce_NONE_to_LOCAL_OPT CT_none
+       | Libnames.DischargeAt _ -> CT_local 
+       | Libnames.NotDeclare -> assert false in
       CT_coercion (local_opt, id_opt, xlate_ident id1,
         xlate_class id2, xlate_class id3)
 (* Not supported
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 1eb22424bb..47d5c5f4d2 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -34,6 +34,7 @@ open Evar_refiner
 open Tactics
 open Clenv
 open Logic
+open Libnames
 open Nametab
 open Omega
 open Contradiction
@@ -151,7 +152,7 @@ let dest_const_apply t =
     | Ind isp       -> IndRef isp
     | _ -> raise Destruct
   in
-  id_of_global (Global.env()) ref, args
+  id_of_global None ref, args
 
 type result = 
   | Kvar of string
@@ -161,14 +162,14 @@ type result =
 
 let destructurate t =
   let c, args = get_applist t in
-  let env = Global.env() in
+(*  let env = Global.env() in*)
   match kind_of_term c, args with
     | Const sp, args ->
-	Kapp (string_of_id (id_of_global env (ConstRef sp)),args)
+	Kapp (string_of_id (id_of_global None (ConstRef sp)),args)
     | Construct csp , args ->
-	Kapp (string_of_id (id_of_global env(ConstructRef csp)), args)
+	Kapp (string_of_id (id_of_global None (ConstructRef csp)), args)
     | Ind isp, args ->
-	Kapp (string_of_id (id_of_global env (IndRef isp)),args)
+	Kapp (string_of_id (id_of_global None (IndRef isp)),args)
     | Var id,[] -> Kvar(string_of_id id)
     | Prod (Anonymous,typ,body), [] -> Kimp(typ,body)
     | Prod (Name _,_,_),[] -> error "Omega: Not a quantifier-free goal"
@@ -200,7 +201,7 @@ let constant dir s =
     Declare.global_reference_in_absolute_module dir id
   with Not_found ->
     anomaly ("Coq_omega: cannot find "^
-	     (Nametab.string_of_qualid (Nametab.make_qualid dir id)))
+	     (Libnames.string_of_qualid (Libnames.make_qualid dir id)))
 
 let arith_constant dir = constant ("Arith"::dir)
 let zarith_constant dir = constant ("ZArith"::dir)
@@ -364,12 +365,12 @@ let make_coq_path dir s =
     try Nametab.locate_in_absolute_module dir id 
     with Not_found ->
       anomaly("Coq_omega: cannot find "^
-	      (Nametab.string_of_qualid(Nametab.make_qualid dir id)))
+	      (Libnames.string_of_qualid(Libnames.make_qualid dir id)))
   in
   match ref with
     | ConstRef sp -> EvalConstRef sp
     | _ -> anomaly ("Coq_omega: "^
-		    (Nametab.string_of_qualid (Nametab.make_qualid dir id))^
+		    (Libnames.string_of_qualid (Libnames.make_qualid dir id))^
 		    " is not a constant")
 
 let sp_Zs = lazy (make_coq_path ["ZArith";"zarith_aux"] "Zs")
@@ -1861,7 +1862,7 @@ let destructure_goal gl =
 let destructure_goal = all_time (destructure_goal)
 
 let omega_solver gl =
-  Library.check_required_module ["Coq";"omega";"Omega"];
+  Library.check_required_library ["Coq";"omega";"Omega"];
   let result = destructure_goal gl in 
   (* if !display_time_flag then begin text_time (); 
      flush Pervasives.stdout end; *)
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index c150a4bfb6..a2798d7a75 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -127,7 +127,7 @@ let constant dir s =
     Declare.global_reference_in_absolute_module dir id
   with Not_found ->
     anomaly ("Quote: cannot find "^
-	     (Nametab.string_of_qualid (Nametab.make_qualid dir id)))
+	     (Libnames.string_of_qualid (Libnames.make_qualid dir id)))
 
 let coq_Empty_vm = lazy (constant ["Quote"] "Empty_vm")
 let coq_Node_vm = lazy (constant ["Quote"] "Node_vm")
@@ -389,7 +389,7 @@ let rec sort_subterm gl l =
   [gl: goal sigma]\\ *)
 
 let quote_terms ivs lc gl =
-  Library.check_required_module ["Coq";"ring";"Quote"];
+  Library.check_required_library ["Coq";"ring";"Quote"];
   let varhash  = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
   let varlist = ref ([] : constr list) in (* list of variables *)
   let counter = ref 1 in (* number of variables created + 1 *)
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 786a746740..db9b00c384 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -15,6 +15,7 @@ open Util
 open Options
 open Term
 open Names
+open Libnames
 open Nameops
 open Reductionops
 open Tacticals
@@ -44,7 +45,7 @@ let constant dir s =
     Declare.global_reference_in_absolute_module dir id
   with Not_found ->
     anomaly ("Ring: cannot find "^
-	     (Nametab.string_of_qualid (Nametab.make_qualid dir id)))
+	     (Libnames.string_of_qualid (Libnames.make_qualid dir id)))
 
 (* Ring theory *)
 let coq_Ring_Theory = lazy (constant ["ring";"Ring_theory"] "Ring_Theory")
@@ -199,14 +200,93 @@ let _ =
    The functions theory_to_obj and obj_to_theory do the conversions
    between theories and environement objects. *)
 
+
+let subst_morph subst morph = 
+  let plusm' = subst_mps subst morph.plusm in
+  let multm' = subst_mps subst morph.multm in
+  let oppm' = option_smartmap (subst_mps subst) morph.oppm in
+    if plusm' == morph.plusm 
+      && multm' == morph.multm 
+      && oppm' == morph.oppm then 
+	morph
+    else
+      { plusm = plusm' ;
+	multm = multm' ;
+	oppm = oppm' ;
+      }
+  
+let subst_set subst cset = 
+  let same = ref true in
+  let copy_subst c newset = 
+    let c' = subst_mps subst c in
+      if not (c' == c) then same := false;
+      ConstrSet.add c' newset
+  in
+  let cset' = ConstrSet.fold copy_subst cset ConstrSet.empty in
+    if !same then cset else cset'
+
+let subst_theory subst th = 
+  let th_equiv' = option_smartmap (subst_mps subst) th.th_equiv in
+  let th_setoid_th' = option_smartmap (subst_mps subst) th.th_setoid_th in
+  let th_morph' = option_smartmap (subst_morph subst) th.th_morph in
+  let th_a' = subst_mps subst th.th_a in                   
+  let th_plus' = subst_mps subst th.th_plus in
+  let th_mult' = subst_mps subst th.th_mult in
+  let th_one' = subst_mps subst th.th_one in
+  let th_zero' = subst_mps subst th.th_zero in
+  let th_opp' = option_smartmap (subst_mps subst) th.th_opp in
+  let th_eq' = subst_mps subst th.th_eq in
+  let th_t' = subst_mps subst th.th_t in          
+  let th_closed' = subst_set subst th.th_closed in
+    if th_equiv' == th.th_equiv 
+      && th_setoid_th' == th.th_setoid_th 
+      && th_morph' == th.th_morph
+      && th_a' == th.th_a
+      && th_plus' == th.th_plus
+      && th_mult' == th.th_mult
+      && th_one' == th.th_one
+      && th_zero' == th.th_zero
+      && th_opp' == th.th_opp
+      && th_eq' == th.th_eq
+      && th_t' == th.th_t
+      && th_closed' == th.th_closed 
+    then 
+      th 
+    else
+    { th_ring = th.th_ring ;  
+      th_abstract = th.th_abstract ;
+      th_setoid = th.th_setoid ;  
+      th_equiv = th_equiv' ;
+      th_setoid_th = th_setoid_th' ;
+      th_morph = th_morph' ;
+      th_a = th_a' ;            
+      th_plus = th_plus' ;
+      th_mult = th_mult' ;
+      th_one = th_one' ;
+      th_zero = th_zero' ;
+      th_opp = th_opp' ;        
+      th_eq = th_eq' ;
+      th_t = th_t' ;            
+      th_closed = th_closed' ;  
+    }
+
+
+let subst_th (_,subst,(c,th as obj)) = 
+  let c' = subst_mps subst c in
+  let th' = subst_theory subst th in
+    if c' == c && th' == th then obj else
+      (c',th')
+
+
 let (theory_to_obj, obj_to_theory) = 
   let cache_th (_,(c, th)) = theories_map_add (c,th)
   and export_th x = Some x in
-  declare_object ("tactic-ring-theory",
-		  { load_function = (fun _ -> ());
-		    open_function = cache_th;
+  declare_object {(default_object "tactic-ring-theory") with
+		    open_function = (fun i o -> if i=1 then cache_th o);
                     cache_function = cache_th;
-		    export_function = export_th })
+		    subst_function = subst_th;
+		    classify_function = (fun (_,x) -> Substitute x);
+		    export_function = export_th }
 
 (* from the set A, guess the associated theory *)
 (* With this simple solution, the theory to use is automatically guessed *)
@@ -647,24 +727,30 @@ module SectionPathSet =
    SectionPathSet; peut-être faudra-t-il la déplacer dans Closure *)
 let constants_to_unfold = 
 (*  List.fold_right SectionPathSet.add *)
-    [ path_of_string "Coq.ring.Ring_normalize.interp_cs";
-      path_of_string "Coq.ring.Ring_normalize.interp_var";
-      path_of_string "Coq.ring.Ring_normalize.interp_vl";
-      path_of_string "Coq.ring.Ring_abstract.interp_acs";
-      path_of_string "Coq.ring.Ring_abstract.interp_sacs";
-      path_of_string "Coq.ring.Quote.varmap_find";
+  let transform s = 
+    let sp = path_of_string s in
+    let dir, id = repr_path sp in
+      Libnames.encode_kn dir id 
+  in
+  List.map transform
+    [ "Coq.ring.Ring_normalize.interp_cs";
+      "Coq.ring.Ring_normalize.interp_var";
+      "Coq.ring.Ring_normalize.interp_vl";
+      "Coq.ring.Ring_abstract.interp_acs";
+      "Coq.ring.Ring_abstract.interp_sacs";
+      "Coq.ring.Quote.varmap_find";
       (* anciennement des Local devenus Definition *)
-      path_of_string "Coq.ring.Ring_normalize.ics_aux";
-      path_of_string "Coq.ring.Ring_normalize.ivl_aux";
-      path_of_string "Coq.ring.Ring_normalize.interp_m";
-      path_of_string "Coq.ring.Ring_abstract.iacs_aux";
-      path_of_string "Coq.ring.Ring_abstract.isacs_aux";
-      path_of_string "Coq.ring.Setoid_ring_normalize.interp_cs";
-      path_of_string "Coq.ring.Setoid_ring_normalize.interp_var";
-      path_of_string "Coq.ring.Setoid_ring_normalize.interp_vl";
-      path_of_string "Coq.ring.Setoid_ring_normalize.ics_aux";
-      path_of_string "Coq.ring.Setoid_ring_normalize.ivl_aux";
-      path_of_string "Coq.ring.Setoid_ring_normalize.interp_m";
+      "Coq.ring.Ring_normalize.ics_aux";
+      "Coq.ring.Ring_normalize.ivl_aux";
+      "Coq.ring.Ring_normalize.interp_m";
+      "Coq.ring.Ring_abstract.iacs_aux";
+      "Coq.ring.Ring_abstract.isacs_aux";
+      "Coq.ring.Setoid_ring_normalize.interp_cs";
+      "Coq.ring.Setoid_ring_normalize.interp_var";
+      "Coq.ring.Setoid_ring_normalize.interp_vl";
+      "Coq.ring.Setoid_ring_normalize.ics_aux";
+      "Coq.ring.Setoid_ring_normalize.ivl_aux";
+      "Coq.ring.Setoid_ring_normalize.interp_m";
     ]
 (*    SectionPathSet.empty *)
 
@@ -782,7 +868,7 @@ let match_with_equiv c = match (kind_of_term c) with
   | _ -> None
 
 let polynom lc gl =
-  Library.check_required_module ["Coq";"ring";"Ring"];
+  Library.check_required_library ["Coq";"ring";"Ring"];
   match lc with 
    (* If no argument is given, try to recognize either an equality or
       a declared relation with arguments c1 ... cn, 
diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml
index 76a6bdf523..42b61a1503 100644
--- a/contrib/romega/const_omega.ml
+++ b/contrib/romega/const_omega.ml
@@ -17,19 +17,19 @@ type result =
 
 let destructurate t =
   let c, args = Term.decompose_app t in
-  let env = Global.env() in
+(*  let env = Global.env() in*)
   match Term.kind_of_term c, args with
     | Term.Const sp, args ->
 	Kapp (Names.string_of_id
-		(Termops.id_of_global env (Nametab.ConstRef sp)),
+		(Nametab.id_of_global None (Libnames.ConstRef sp)),
               args)
     | Term.Construct csp , args ->
 	Kapp (Names.string_of_id
-		(Termops.id_of_global env (Nametab.ConstructRef csp)),
+		(Nametab.id_of_global None (Libnames.ConstructRef csp)),
 	        args)
     | Term.Ind isp, args ->
 	Kapp (Names.string_of_id
-		(Termops.id_of_global env (Nametab.IndRef isp)),args)
+		(Nametab.id_of_global None (Libnames.IndRef isp)),args)
     | Term.Var id,[] -> Kvar(Names.string_of_id id)
     | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body)
     | Term.Prod (Names.Name _,_,_),[] ->
@@ -42,12 +42,12 @@ let dest_const_apply t =
   let f,args = Term.decompose_app t in
   let ref = 
   match Term.kind_of_term f with 
-    | Term.Const sp         -> Nametab.ConstRef sp
-    | Term.Construct csp -> Nametab.ConstructRef csp
-    | Term.Ind isp       -> Nametab.IndRef isp
+    | Term.Const sp         -> Libnames.ConstRef sp
+    | Term.Construct csp -> Libnames.ConstructRef csp
+    | Term.Ind isp       -> Libnames.IndRef isp
     | _ -> raise Destruct
   in
-  Termops.id_of_global (Global.env()) ref, args
+  Nametab.id_of_global None ref, args
 
 let recognize_number t =
   let rec loop t =
@@ -65,7 +65,7 @@ let recognize_number t =
 let constant dir s =
   try
     Declare.global_absolute_reference
-      (Names.make_path
+      (Libnames.make_path
         (Names.make_dirpath (List.map Names.id_of_string (List.rev dir)))
         (Names.id_of_string s))
   with e -> print_endline (String.concat "." dir); print_endline s; 
diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml
index f87f3db964..e6e7074aa8 100644
--- a/contrib/romega/refl_omega.ml
+++ b/contrib/romega/refl_omega.ml
@@ -818,7 +818,7 @@ let destructure_hyps gl =
   loop (pf_ids_of_hyps gl) (pf_hyps gl) gl
 
 let omega_solver gl =
-  Library.check_required_module ["Coq";"romega";"ROmega"];
+  Library.check_required_library ["Coq";"romega";"ROmega"];
   let concl = pf_concl gl in
   let rec loop t =
     match destructurate t with
diff --git a/contrib/xml/xmlcommand.ml4 b/contrib/xml/xmlcommand.ml4
index 3c06c00dae..a2baceade2 100644
--- a/contrib/xml/xmlcommand.ml4
+++ b/contrib/xml/xmlcommand.ml4
@@ -78,16 +78,16 @@ let extract_nparams pack =
 (* than that could exists in cooked form with the same name in a super        *)
 (* section of the actual section                                              *)
 let could_have_namesakes o sp =      (* namesake = omonimo in italian *)
- let module N = Nametab in
+ let module L = Libnames in
  let module D = Declare in
   let tag = Libobject.object_tag o in
    print_if_verbose ("Object tag: " ^ tag ^ "\n") ;
    match tag with
       "CONSTANT" ->
         (match D.constant_strength sp with
-          | N.DischargeAt _  -> false (* a local definition *)
-          | N.NotDeclare     -> false (* not a definition *)
-          | N.NeverDischarge -> true  (* a non-local one    *)
+          | L.DischargeAt _  -> false (* a local definition *)
+          | L.NotDeclare     -> false (* not a definition *)
+          | L.NeverDischarge -> true  (* a non-local one    *)
         )
     | "PARAMETER"                 (* axioms and                               *)
     | "INDUCTIVE"       -> true   (* mutual inductive types are never local   *)
@@ -100,9 +100,9 @@ let could_have_namesakes o sp =      (* namesake = omonimo in italian *)
 (* section path is sp                                                         *)
 let uri_of_path sp tag =
  let module N = Names in
- let module No = Nameops in
+ let module L = Libnames in
   let ext_of_sp sp = ext_of_tag tag in
-  let dir0 = No.extend_dirpath (No.dirpath sp) (No.basename sp) in
+  let dir0 = L.extend_dirpath (L.dirpath sp) (L.basename sp) in
   let dir = List.map N.string_of_id (List.rev (N.repr_dirpath dir0)) in
    "cic:/" ^ (String.concat "/" dir) ^ "." ^ (ext_of_sp sp)
 ;;
@@ -260,6 +260,8 @@ let print_term inner_types l env csr =
  let module N = Names in
  let module E = Environ in
  let module T = Term in
+ let module Nt = Nametab in
+ let module L = Libnames in
  let module X = Xml in
  let module R = Retyping in
   let rec names_to_ids =
@@ -419,23 +421,27 @@ let print_term inner_types l env csr =
           (fun x i -> [< (term_display idradix false l env x); i >]) t [<>])
        >]
 )
-   | T.Const sp ->
-      X.xml_empty "CONST"
+   | T.Const kn ->
+       let sp = Nt.sp_of_global None (L.ConstRef kn) in  
+	 X.xml_empty "CONST"
        (add_sort_attribute false
         ["uri",(uri_of_path sp Constant) ; "id", next_id])
-   | T.Ind (sp,i) ->
+   | T.Ind (kn,i) ->
+      let sp = Nt.sp_of_global None (L.IndRef(kn,0)) in  
       X.xml_empty "MUTIND"
        ["uri",(uri_of_path sp Inductive) ;
         "noType",(string_of_int i) ;
         "id", next_id]
-   | T.Construct ((sp,i),j) ->
+   | T.Construct ((kn,i),j) ->
+      let sp = Nt.sp_of_global None (L.IndRef(kn,0)) in  
       X.xml_empty "MUTCONSTRUCT"
        (add_sort_attribute false
         ["uri",(uri_of_path sp Inductive) ;
          "noType",(string_of_int i) ;
          "noConstr",(string_of_int j) ;
          "id", next_id])
-   | T.Case ({T.ci_ind=(sp,i)},ty,term,a) ->
+   | T.Case ({T.ci_ind=(kn,i)},ty,term,a) ->
+      let sp = Nt.sp_of_global None (L.IndRef(kn,0)) in  
       let (uri, typeno) = (uri_of_path sp Inductive),i in
        X.xml_nempty "MUTCASE"
         (add_sort_attribute true
@@ -709,22 +715,24 @@ let print (_,qid as locqid) fn =
  let module G = Global in
  let module N = Names in
  let module Nt = Nametab in
+ let module Ln = Libnames in
  let module T = Term in
  let module X = Xml in
-  let (_,id) = Nt.repr_qualid qid in
+  let (_,id) = Ln.repr_qualid qid in
   let glob_ref = Nametab.global locqid in
-  let env = (Safe_typing.env_of_safe_env (G.safe_env ())) in
+  let env = G.env () in
   reset_ids () ;
   let inner_types = ref [] in
   let sp,tag,pp_cmds =
    match glob_ref with
-      Nt.VarRef id ->
+      Ln.VarRef id ->
         let sp = Declare.find_section_variable id in
        let (_,body,typ) = G.lookup_named id in
         sp,Variable,print_variable id body (T.body_of_type typ) env inner_types
-    | Nt.ConstRef sp ->
+    | Ln.ConstRef kn ->
+       let sp = Nt.sp_of_global None glob_ref in
        let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
-        G.lookup_constant sp in
+        G.lookup_constant kn in
        let hyps = string_list_of_named_context_list hyps in
        let typ = T.body_of_type typ in
         sp,Constant,
@@ -733,14 +741,15 @@ let print (_,qid as locqid) fn =
             None ->   print_axiom id typ [] hyps env inner_types
           | Some c -> print_definition id c typ [] hyps env inner_types
         end
-    | Nt.IndRef (sp,_) ->
+    | Ln.IndRef (kn,_) ->
+       let sp = Nt.sp_of_global None (Ln.IndRef(kn,0)) in  
        let {D.mind_packets=packs ;
             D.mind_hyps=hyps;
-            D.mind_finite=finite} = G.lookup_mind sp in
+            D.mind_finite=finite} = G.lookup_mind kn in
         let hyps = string_list_of_named_context_list hyps in
          sp,Inductive,
           print_mutual_inductive finite packs [] hyps env inner_types
-    | Nt.ConstructRef _ ->
+    | Ln.ConstructRef _ ->
        Util.anomaly ("print: this should not happen")
   in
    Xml.pp pp_cmds fn ;
@@ -802,11 +811,11 @@ let mkfilename dn sp ext =
   let module L = Library in
   let module S = System in
   let module N = Names in
-  let module No = Nameops in
+  let module Ln = Libnames in
    match dn with
       None         -> None
     | Some basedir ->
-	let dir0 = No.extend_dirpath (No.dirpath sp) (No.basename sp) in
+	let dir0 = Ln.extend_dirpath (Ln.dirpath sp) (Ln.basename sp) in
 	let dir = List.map N.string_of_id (List.rev (N.repr_dirpath dir0)) in
        Some (basedir ^ join_dirs basedir dir ^ "." ^ ext)
 ;;
@@ -823,7 +832,7 @@ let mkfilename dn sp ext =
 (* Note: it is printed only the uncooked available form of the object plus  *)
 (*       the list of parameters of the object deduced from it's most cooked *)
 (*       form                                                               *)
-let print_object lobj id sp dn fv env =
+let print_object lobj id (sp,kn) dn fv env =
  let module D = Declarations in
  let module E = Environ in
  let module G = Global in
@@ -840,7 +849,7 @@ let print_object lobj id sp dn fv env =
         "CONSTANT"  (* = Definition, Theorem *)
       | "PARAMETER" (* = Axiom *) ->
           let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
-           G.lookup_constant sp
+           G.lookup_constant kn
           in
            let hyps = string_list_of_named_context_list hyps in
            let typ = T.body_of_type typ in
@@ -854,7 +863,7 @@ let print_object lobj id sp dn fv env =
             {D.mind_packets=packs ;
              D.mind_hyps = hyps;
              D.mind_finite = finite
-            } = G.lookup_mind sp
+            } = G.lookup_mind kn
            in
             let hyps = string_list_of_named_context_list hyps in
              print_mutual_inductive finite packs fv hyps env inner_types
@@ -892,14 +901,14 @@ let print_object lobj id sp dn fv env =
 (* print via print_node all the nodes (leafs excluded if bprintleaf is false) *)(* in state                                                                   *)
 let rec print_library_segment state bprintleaf dn =
   List.iter
-   (function (sp, node) ->
-     print_if_verbose ("Print_library_segment: " ^ Names.string_of_path sp ^ "\n") ;
-     print_node node (Nameops.basename sp) sp bprintleaf dn ;
+   (function ((sp,_ as oname), node) ->
+     print_if_verbose ("Print_library_segment: " ^ Libnames.string_of_path sp ^ "\n") ;
+     print_node node (Libnames.basename sp) oname bprintleaf dn ;
      print_if_verbose "\n"
    ) (List.rev state)
 (* print_node node id section_path bprintleaf directory_name             *)
 (* prints a single node (and all it's subnodes via print_library_segment *)
-and print_node n id sp bprintleaf dn =
+and print_node n id (sp,kn as oname) bprintleaf dn =
  let module L = Lib in
   match n with
      L.Leaf o ->
@@ -914,14 +923,14 @@ try
             begin
              (* this is an uncooked term *)
              print_if_verbose ("OK, stampo solo questa volta " ^ Names.string_of_id id ^ "\n") ;
-             print_object o id sp dn !pvars !cumenv ;
+             print_object o id oname dn !pvars !cumenv ;
              printed := id::!printed
             end
            else
             begin
              (* this is a local term *)
              print_if_verbose ("OK, stampo " ^ Names.string_of_id id ^ "\n") ;
-             print_object o id sp dn !pvars !cumenv
+             print_object o id oname dn !pvars !cumenv
             end
 with _ -> print_if_verbose ("EXCEPTION RAISED!!!\n");
           end
@@ -931,11 +940,11 @@ with _ -> print_if_verbose ("EXCEPTION RAISED!!!\n");
            print_if_verbose ("Suppongo gia' stampato " ^ Names.string_of_id id ^ "\n")
           end
        end
-   | L.OpenedSection (dir,_) ->
-       let id = snd (Nameops.split_dirpath dir) in
+   | L.OpenedSection ((dir,_),_) ->
+       let id = snd (Libnames.split_dirpath dir) in
        print_if_verbose ("OpenDir " ^ Names.string_of_id id ^ "\n")
    | L.ClosedSection (_,dir,state) ->
-      let id = snd (Nameops.split_dirpath dir) in
+      let id = snd (Libnames.split_dirpath dir) in
       print_if_verbose("ClosedDir " ^ Names.string_of_id id ^ "\n") ;
       if bprintleaf then
        begin
@@ -948,8 +957,12 @@ with _ -> print_if_verbose ("EXCEPTION RAISED!!!\n");
          | he::tl -> pvars := tl
        end ;
       print_if_verbose "/ClosedDir\n"
-   | L.Module s ->
-      print_if_verbose ("Module " ^ (Names.string_of_dirpath s) ^ "\n")
+   | L.CompilingModule (s,_) ->
+      print_if_verbose ("Library " ^ (Names.string_of_dirpath s) ^ "\n")
+   | L.OpenedModtype ((s,_), _) ->
+      print_if_verbose ("Open Module Type " ^ (Names.string_of_dirpath s) ^ "\n")
+   | L.OpenedModule ((s,_), _) -> 
+      print_if_verbose ("Open Module " ^ (Names.string_of_dirpath s) ^ "\n")
    | L.FrozenState _ ->
       print_if_verbose ("FrozenState\n")
 ;;
@@ -977,20 +990,23 @@ let print_closed_section s ls dn =
 (* and terms of the module d                                                 *)
 (* Note: the terms are printed in their uncooked form plus the informations  *)
 (* on the parameters of their most cooked form                               *)
-let printModule (loc,qid) dn =
+let printLibrary (loc,qid) dn =
+ let module N = Names in
  let module L = Library in
- let module N = Nametab in
+ let module Ln = Libnames in
+ let module Dm = Declaremods in
+ let module Nt = Nametab in
  let module X = Xml in
 
   let (_,dir_path,_) = L.locate_qualified_library qid in
 
-  let str = N.string_of_qualid qid in 
-  let ls = L.module_segment (Some dir_path) in
-   print_if_verbose ("MODULE_BEGIN " ^ str ^ " " ^
-    (L.module_full_filename dir_path) ^ "\n") ;
+  let str = Ln.string_of_qualid qid in 
+  let ls = Dm.module_objects (N.MPfile dir_path) in
+   print_if_verbose ("LIBRARY_BEGIN " ^ str ^ " " ^
+    (L.library_full_filename dir_path) ^ "\n") ;
    print_closed_section str (List.rev ls) dn ;
-   print_if_verbose ("MODULE_END " ^ str ^ " " ^
-    (L.module_full_filename dir_path) ^ "\n")
+   print_if_verbose ("LIBRARY_END " ^ str ^ " " ^
+    (L.library_full_filename dir_path) ^ "\n")
 ;;
 
 (* printSection identifier directory_name                                    *)
@@ -1003,30 +1019,30 @@ let printModule (loc,qid) dn =
 let printSection id dn =
  let module L = Library in
  let module N = Names in
- let module No = Nameops in
+ let module Ln = Libnames in
  let module X = Xml in
   let sp = Lib.make_path id in
   let ls =
    let rec find_closed_section =
     function
        [] -> raise Not_found
-     | (_,Lib.ClosedSection (_,dir,ls))::_ when snd (No.split_dirpath dir) = id
+     | (_,Lib.ClosedSection (_,dir,ls))::_ when snd (Ln.split_dirpath dir) = id
 	 -> ls
      | _::t -> find_closed_section t
    in
-    print_string ("Searching " ^ Names.string_of_path sp ^ "\n") ;
+    print_string ("Searching " ^ Ln.string_of_path sp ^ "\n") ;
     find_closed_section (Lib.contents_after None)
   in
   let str = N.string_of_id id in 
-   print_if_verbose ("SECTION_BEGIN " ^ str ^ " " ^ N.string_of_path sp ^ "\n");
+   print_if_verbose ("SECTION_BEGIN " ^ str ^ " " ^ Ln.string_of_path sp ^ "\n");
    print_closed_section str ls dn ;
-   print_if_verbose ("SECTION_END " ^ str ^ " " ^ N.string_of_path sp ^ "\n")
+   print_if_verbose ("SECTION_END " ^ str ^ " " ^ Ln.string_of_path sp ^ "\n")
 ;;
 
 (* print All () prints what is the structure of the current environment of *)
 (* Coq. No terms are printed. Useful only for debugging                    *)
 let printAll () =
- let state = Library.module_segment None in
+ let state = Lib.contents_after None in
   let oldverbose = !verbose in
    verbose := true ;
    print_library_segment state false None ;
diff --git a/contrib/xml/xmlcommand.mli b/contrib/xml/xmlcommand.mli
index 07335ea6a5..485bb93c27 100644
--- a/contrib/xml/xmlcommand.mli
+++ b/contrib/xml/xmlcommand.mli
@@ -28,7 +28,7 @@
 (* Note: it is printed only (and directly) the most cooked available      *)
 (*       form of the definition (all the parameters are                   *)
 (*       lambda-abstracted, but the object can still refer to variables)  *)
-val print : Nametab.qualid Util.located -> string option -> unit
+val print : Libnames.qualid Util.located -> string option -> unit
 
 (* show dest                                                  *)
 (*  where dest is either None (for stdout) or (Some filename) *)
@@ -39,14 +39,14 @@ val show : string option -> unit
 (* Coq. No terms are printed. Useful only for debugging                    *)
 val printAll : unit -> unit
 
-(* printModule identifier directory_name *)
-(*  where identifier     is the qualified name of a module d                 *)
+(* printLibrary identifier directory_name *)
+(*  where identifier     is the qualified name of a library d                 *)
 (*  and   directory_name is the directory in which to root all the xml files *)
 (* prints all the xml files and directories corresponding to the subsections *)
-(* and terms of the module d                                                 *)
+(* and terms of the library d                                                 *)
 (* Note: the terms are printed in their uncooked form plus the informations  *)
 (* on the parameters of their most cooked form                               *)
-val printModule : Nametab.qualid Util.located -> string option -> unit
+val printLibrary : Libnames.qualid Util.located -> string option -> unit
 
 (* printSection identifier directory_name *)
 (*  where identifier     is the name of a closed section d                   *)
diff --git a/contrib/xml/xmlentries.ml4 b/contrib/xml/xmlentries.ml4
index d812697023..876da02e2e 100644
--- a/contrib/xml/xmlentries.ml4
+++ b/contrib/xml/xmlentries.ml4
@@ -88,7 +88,7 @@ VERNAC COMMAND EXTEND Xml
 | [ "Print" "XML" "All" ] -> [ Xmlcommand.printAll () ]
 
 | [ "Print" "XML" "Module" diskname(dn) qualid(id) ] ->
-    [ Xmlcommand.printModule id dn ]
+    [ Xmlcommand.printLibrary id dn ]
 
 | [ "Print" "XML" "Section" diskname(dn) ident(id) ] ->
     [ Xmlcommand.printSection id dn ]