GROS COMMIT:

 - reduction du noyau (variables existentielles, fonctions auxiliaires
   pour inventer des noms, etc. deplacees hors de kernel/)
 - changement de noms de constructeurs des constr (suppression de "Is" et
   "Mut")


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

18 files changed, 585 insertions, 964 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 1c034190e..1f5b69458 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -11,19 +11,23 @@
 open Pp
 open Util
 open Names
+open Nameops
 open Term
 open Sign
 open Declarations
 open Inductive
+open Indtypes
 open Reduction
 open Type_errors
 open Typeops
 open Libobject
 open Lib
 open Impargs
-open Indrec
 open Nametab
 open Library
+open Safe_typing
+
+(**********************************************)
 
 (* For [DischargeAt (dir,n)], [dir] is the minimum prefix that a
    construction keeps in its name (if persistent), or the section name
@@ -41,20 +45,11 @@ let depth_of_strength = function
   | NeverDischarge -> 0
   | NotDeclare -> assert false
 
-let restrict_path n sp =
-  let dir, s, k = repr_path sp in
-  let dir' = list_lastn n (repr_dirpath dir) in
-  Names.make_path (make_dirpath dir') s k
-
 let make_strength_0 () = 
   let depth = Lib.sections_depth () in
   let cwd = Lib.cwd() in
   if depth > 0 then DischargeAt (cwd, depth) else NeverDischarge
 
-let extract_dirpath_prefix n dir =
-  let dir = repr_dirpath dir in
-  make_dirpath (list_firstn (List.length dir -n) dir)
-
 let make_strength_1 () =
   let depth = Lib.sections_depth () in
   let cwd = Lib.cwd() in
@@ -74,37 +69,32 @@ type section_variable_entry =
   | SectionLocalDef of constr
   | SectionLocalAssum of constr
 
-type variable_declaration = section_variable_entry * strength
+type variable_declaration = dir_path * section_variable_entry * strength
 
 type checked_section_variable = constr option * types * Univ.constraints
 
 type checked_variable_declaration =
-    checked_section_variable * strength
+    dir_path * checked_section_variable * strength
 
-let vartab =
-  ref ((Spmap.empty, []) :
-       (identifier * checked_variable_declaration) Spmap.t * section_path list)
-
-let current_section_context () =
-  List.map (fun sp -> (basename sp, sp)) (snd !vartab)
+let vartab = ref (Idmap.empty : checked_variable_declaration Idmap.t)
 
 let _ = Summary.declare_summary "VARIABLE"
 	  { Summary.freeze_function = (fun () -> !vartab);
 	    Summary.unfreeze_function = (fun ft -> vartab := ft);
-	    Summary.init_function = (fun () -> vartab := (Spmap.empty, []));
+	    Summary.init_function = (fun () -> vartab := Idmap.empty);
 	    Summary.survive_section = false }
 
-let cache_variable (sp,(id,(d,str))) =
+let cache_variable (sp,(id,(p,d,str))) =
   (* Constr raisonne sur les noms courts *)
-  if List.mem_assoc id (current_section_context ()) then
-    errorlabstrm "cache_variable"
-      [< pr_id (basename sp); 'sTR " already exists" >];
-  let vd = match d with (* Fails if not well-typed *)
+  if Idmap.mem id !vartab then
+    errorlabstrm "cache_variable" [< pr_id id; 'sTR " already exists" >];
+  let cst = match d with (* Fails if not well-typed *)
     | SectionLocalAssum ty -> Global.push_named_assum (id,ty)
-    | SectionLocalDef c -> Global.push_named_def (id,c)
-  in
-  Nametab.push 0 (restrict_path 0 sp) (VarRef sp);
-  vartab := let (m,l) = !vartab in (Spmap.add sp (id,(vd,str)) m, sp::l)
+    | SectionLocalDef c -> Global.push_named_def (id,c) in
+  let (_,bd,ty) = Global.lookup_named id in
+  let vd = (bd,ty,cst) in
+  Nametab.push 0 (restrict_path 0 sp) (VarRef id);
+  vartab := Idmap.add id (p,vd,str) !vartab
 
 let (in_variable, out_variable) =
   let od = {
@@ -116,23 +106,23 @@ let (in_variable, out_variable) =
   declare_object ("VARIABLE", od)
 
 let declare_variable id obj =
-  let sp = add_leaf id CCI (in_variable (id,obj)) in
-  if is_implicit_args() then declare_var_implicits sp;
+  let sp = add_leaf id (in_variable (id,obj)) in
+  if is_implicit_args() then declare_var_implicits id;
   sp
 
 (* Parameters. *)
 
 let cache_parameter (sp,c) =
-  if Nametab.exists_cci sp then
-    errorlabstrm "cache_parameter"
-      [< pr_id (basename sp); 'sTR " already exists" >];
-  Global.add_parameter sp c (current_section_context ());
+  (if Nametab.exists_cci sp then
+    let (_,id) = repr_path sp in
+    errorlabstrm "cache_parameter" [< pr_id id; 'sTR " already exists" >]);
+  Global.add_parameter sp c;
   Nametab.push 0 sp (ConstRef sp)
 
 let load_parameter (sp,_) =
-  if Nametab.exists_cci sp then
-    errorlabstrm "cache_parameter"
-      [< pr_id (basename sp); 'sTR " already exists" >];
+  (if Nametab.exists_cci sp then
+    let (_,id) = repr_path sp in
+    errorlabstrm "cache_parameter" [< pr_id id; 'sTR " already exists" >]);
   Nametab.push 1 sp (ConstRef sp)
 
 let open_parameter (sp,_) =
@@ -153,7 +143,7 @@ let (in_parameter, out_parameter) =
   declare_object ("PARAMETER", od)
 
 let declare_parameter id c =
-  let sp = add_leaf id CCI (in_parameter c) in 
+  let sp = add_leaf id (in_parameter c) in 
   if is_implicit_args() then declare_constant_implicits sp;
   sp
 
@@ -174,16 +164,15 @@ let _ = Summary.declare_summary "CONSTANT"
 	    Summary.survive_section = false }
 
 let cache_constant (sp,(cdt,stre)) =
-  if Nametab.exists_cci sp then
-    errorlabstrm "cache_constant"
-      [< pr_id (basename sp); 'sTR " already exists" >] ;
-  let sc = current_section_context() in
+  (if Nametab.exists_cci sp then
+    let (_,id) = repr_path sp in
+    errorlabstrm "cache_constant" [< pr_id id; 'sTR " already exists" >]);
   begin match cdt with 
-    | ConstantEntry ce -> Global.add_constant sp ce sc
-    | ConstantRecipe r -> Global.add_discharged_constant sp r sc
+    | ConstantEntry ce -> Global.add_constant sp ce
+    | ConstantRecipe r -> Global.add_discharged_constant sp r
   end;
   (match stre with
-    | DischargeAt (sp',n) when not (is_dirpath_prefix_of sp' (Lib.cwd ())) ->
+    | DischargeAt (dp,n) when not (is_dirpath_prefix_of dp (Lib.cwd ())) ->
         (* Only qualifications including the sections segment from the current
            section to the discharge section is available for Remark & Fact *)
         Nametab.push (n-Lib.sections_depth()) sp (ConstRef sp)
@@ -196,9 +185,9 @@ let cache_constant (sp,(cdt,stre)) =
 (* At load-time, the segment starting from the module name to the discharge *)
 (* section (if Remark or Fact) is needed to access a construction *)
 let load_constant (sp,(ce,stre)) =
-  if Nametab.exists_cci sp then
-    errorlabstrm "cache_constant"
-      [< pr_id (basename sp); 'sTR " already exists" >] ;
+  (if Nametab.exists_cci sp then
+    let (_,id) = repr_path sp in
+    errorlabstrm "cache_constant" [< pr_id id; 'sTR " already exists" >]);
   csttab := Spmap.add sp stre !csttab;
   Nametab.push (depth_of_strength stre + 1) sp (ConstRef sp)
 
@@ -235,7 +224,7 @@ let hcons_constant_declaration = function
 
 let declare_constant id cd =
   (* let cd = hcons_constant_declaration cd in *)
-  let sp = add_leaf id CCI (in_constant cd) in
+  let sp = add_leaf id (in_constant cd) in
   if is_implicit_args() then declare_constant_implicits sp;
   sp
 
@@ -245,8 +234,8 @@ let redeclare_constant sp cd =
 
 (* Inductives. *)
 
-
 let inductive_names sp mie =
+  let (dp,_) = repr_path sp in
   let names, _ = 
     List.fold_left
       (fun (names, n) ind ->
@@ -254,23 +243,23 @@ let inductive_names sp mie =
 	 let names, _ =
 	   List.fold_left
 	     (fun (names, p) id ->
-		let sp = Names.make_path (dirpath sp) id CCI in
+		let sp = Names.make_path dp id in
 		((sp, ConstructRef (indsp,p)) :: names, p+1))
 	     (names, 1) ind.mind_entry_consnames in
-	 let sp = Names.make_path (dirpath sp) ind.mind_entry_typename CCI in
+	 let sp = Names.make_path dp ind.mind_entry_typename in
 	 ((sp, IndRef indsp) :: names, n+1))
       ([], 0) mie.mind_entry_inds
   in names
 
 let check_exists_inductive (sp,_) =
   if Nametab.exists_cci sp then
-    errorlabstrm "cache_inductive"
-      [< pr_id (basename sp); 'sTR " already exists" >]
+    let (_,id) = repr_path sp in
+    errorlabstrm "cache_inductive" [< pr_id id; 'sTR " already exists" >]
 
 let cache_inductive (sp,mie) =
   let names = inductive_names sp mie in
   List.iter check_exists_inductive names;
-  Global.add_mind sp mie (current_section_context ());
+  Global.add_mind sp mie;
   List.iter 
     (fun (sp, ref) -> Nametab.push 0 sp ref)
     names
@@ -314,7 +303,7 @@ let declare_mind mie =
     | ind::_ -> ind.mind_entry_typename
     | [] -> anomaly "cannot declare an empty list of inductives"
   in
-  let sp = add_leaf id CCI (in_inductive mie) in
+  let sp = add_leaf id (in_inductive mie) in
   if is_implicit_args() then declare_mib_implicits sp;
   sp
 
@@ -329,18 +318,19 @@ let constant_strength sp = Spmap.find sp !csttab
 let constant_or_parameter_strength sp =
   try constant_strength sp with Not_found -> NeverDischarge
 
-let get_variable sp = 
-  let (id,((c,ty,cst),str)) = Spmap.find sp (fst !vartab) in
-(*  let (c,ty) = Global.lookup_named id in*)
+let get_variable id = 
+  let (p,(c,ty,cst),str) = Idmap.find id !vartab in
   ((id,c,ty),str)
 
-let get_variable_with_constraints sp = 
-  let (id,((c,ty,cst),str)) = Spmap.find sp (fst !vartab) in
-(*  let (c,ty) = Global.lookup_named id in*)
+let get_variable_with_constraints id = 
+  let (p,(c,ty,cst),str) = Idmap.find id !vartab in
   ((id,c,ty),cst,str)
 
-let variable_strength sp =
-  let _,(_,str) = Spmap.find sp (fst !vartab) in str
+let variable_strength id =
+  let (_,_,str) = Idmap.find id !vartab in str
+
+let find_section_variable id =
+  let (p,_,_) = Idmap.find id !vartab in Names.make_path p id
 
 (* Global references. *)
 
@@ -367,54 +357,33 @@ let mind_oper_of_id sp id mib =
     mib.mind_packets
 
 let context_of_global_reference = function
-  | VarRef sp -> []
+  | VarRef id -> []
   | ConstRef sp -> (Global.lookup_constant sp).const_hyps
   | IndRef (sp,_) -> (Global.lookup_mind sp).mind_hyps
   | ConstructRef ((sp,_),_) -> (Global.lookup_mind sp).mind_hyps
 
-let find_section_variable id =
-  let l =
-    Spmap.fold
-      (fun sp (id',_) hyps -> if id=id' then sp::hyps else hyps)
-      (fst !vartab) [] in
-  match l with
-    | [] -> raise Not_found
-    | [sp] -> sp
-    | _ -> anomaly "Several section variables with same base name"
-
 let reference_of_constr c = match kind_of_term c with
-  | IsConst sp -> ConstRef sp
-  | IsMutInd ind_sp -> IndRef ind_sp
-  | IsMutConstruct cstr_cp -> ConstructRef cstr_cp
-  | IsVar id -> VarRef (find_section_variable id)
+  | Const sp -> ConstRef sp
+  | Ind ind_sp -> IndRef ind_sp
+  | Construct cstr_cp -> ConstructRef cstr_cp
+  | Var id -> VarRef id
   |  _ -> raise Not_found
 
 let last_section_hyps dir =
-  List.fold_right
-    (fun sp hyps -> if dirpath sp = dir then basename sp :: hyps else hyps)
-    (snd !vartab) []
-
-let rec find_var id = function
-  | [] -> raise Not_found
-  | sp::l -> if basename sp = id then sp else find_var id l
-
-let extract_instance ref args =
-  let hyps = context_of_global_reference ref in
-  let hyps0 = current_section_context () in
-  let na = Array.length args in
-  let rec peel n acc = function
-    | (sp,None,_ as d)::hyps ->
-	if List.mem_assoc (basename sp) hyps0 then peel (n-1) acc hyps
-	else peel (n-1) (args.(n)::acc) hyps
-    | (_,Some _,_)::hyps -> peel n acc hyps
-    | [] -> Array.of_list acc
-  in peel (na-1) [] hyps
+  fold_named_context
+    (fun (id,_,_) sec_ids ->
+      try
+        let (p,_,_) = Idmap.find id !vartab in
+        if dir=p then id::sec_ids else sec_ids
+      with Not_found -> sec_ids)
+    (Environ.named_context (Global.env()))
+    []
 
 let constr_of_reference = function
-  | VarRef sp -> mkVar (basename sp)
+  | VarRef id -> mkVar id
   | ConstRef sp -> mkConst sp
-  | ConstructRef sp -> mkMutConstruct sp
-  | IndRef sp -> mkMutInd sp
+  | ConstructRef sp -> mkConstruct sp
+  | IndRef sp -> mkInd sp
 
 let construct_absolute_reference sp =
   constr_of_reference (Nametab.absolute_reference sp)
@@ -427,7 +396,7 @@ let construct_reference env id =
   try
     mkVar (let _ = Environ.lookup_named id env in id)
   with Not_found ->
-    let ref = Nametab.sp_of_id CCI id in
+    let ref = Nametab.sp_of_id id in
     constr_of_reference ref
 
 let global_qualified_reference qid =
@@ -442,8 +411,10 @@ let global_reference_in_absolute_module dir id =
 let global_reference id = 
   construct_reference (Global.env()) id
 
+let dirpath sp = let (p,_) = repr_path sp in p
+
 let dirpath_of_global = function
-  | VarRef sp -> dirpath sp
+  | VarRef id -> empty_dirpath
   | ConstRef sp -> dirpath sp
   | IndRef (sp,_) -> dirpath sp
   | ConstructRef ((sp,_),_) -> dirpath sp
@@ -460,80 +431,3 @@ let is_global id =
     is_dirpath_prefix_of (dirpath_of_global osp) (Lib.cwd())
   with Not_found -> 
     false
-
-let path_of_constructor_path ((sp,tyi),ind) =
-   let mib = Global.lookup_mind sp in
-   let mip = mind_nth_type_packet mib tyi in 
-   let (pa,_,k) = repr_path sp in 
-   Names.make_path pa (mip.mind_consnames.(ind-1)) k 
-
-let path_of_inductive_path (sp,tyi) =
-  if tyi = 0 then sp
-  else
-    let mib = Global.lookup_mind sp in
-    let mip = mind_nth_type_packet mib tyi in 
-    let (pa,_,k) = repr_path sp in 
-    Names.make_path pa (mip.mind_typename) k 
-
-(*s Eliminations. *)
-
-let eliminations =
-  [ (InProp,"_ind") ; (InSet,"_rec") ; (InType,"_rect") ]
-
-let elimination_suffix = function
-  | InProp -> "_ind"
-  | InSet  -> "_rec"
-  | InType -> "_rect"
-
-let make_elimination_ident id s = add_suffix id (elimination_suffix s)
-  
-let declare_one_elimination mispec =
-  let mindstr = string_of_id (mis_typename mispec) in
-  let declare na c =
-    let _ = declare_constant (id_of_string na)
-      (ConstantEntry
-        { const_entry_body = c;
-          const_entry_type = None;
-          const_entry_opaque = false }, 
-       NeverDischarge) in
-    Options.if_verbose pPNL [< 'sTR na; 'sTR " is defined" >]
-  in
-  let env = Global.env () in
-  let sigma = Evd.empty in
-  let elim_scheme = build_indrec env sigma mispec in
-  let npars = mis_nparams mispec in
-  let make_elim s = instanciate_indrec_scheme s npars elim_scheme in
-  let kelim = mis_kelim mispec in
-  List.iter
-    (fun (sort,suff) -> 
-       if List.mem sort kelim then
-	 declare (mindstr^suff) (make_elim (new_sort_in_family sort)))
-    eliminations
-
-let declare_eliminations sp =
-  let mib = Global.lookup_mind sp in
-(*
-  let ids = ids_of_named_context mib.mind_hyps in
-  if not (list_subset ids (ids_of_named_context (Global.named_context ()))) then    error ("Declarations of elimination scheme outside the section "^
-    "of the inductive definition is not implemented");
-*)
-  for i = 0 to Array.length mib.mind_packets - 1 do
-    if mind_type_finite mib i then
-      let mispec = Global.lookup_mind_specif (sp,i) in 
-      declare_one_elimination mispec
-  done
-
-(* Look up function for the default elimination constant *)
-
-let lookup_eliminator env ind_sp s =
-  let path = path_of_inductive_path ind_sp in
-  let dir, base,k = repr_path path in
-  let id = add_suffix base (elimination_suffix s) in
-  (* Try first to get an eliminator defined in the same section as the *)
-  (* inductive type *)
-  try construct_absolute_reference (Names.make_path dir id k)
-  with Not_found ->
-  (* Then try to get a user-defined eliminator in some other places *)
-  (* using short name (e.g. for "eq_rec") *)
-  construct_reference env id
-  
diff --git a/library/declare.mli b/library/declare.mli
index be5678f7f..c57dd2079 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -13,8 +13,10 @@ open Names
 open Term
 open Sign
 open Declarations
-open Inductive
+open Indtypes
+open Safe_typing
 open Library
+open Nametab
 (*i*)
 
 (* This module provides the official functions to declare new variables, 
@@ -33,9 +35,9 @@ type section_variable_entry =
   | SectionLocalDef of constr
   | SectionLocalAssum of constr
 
-type variable_declaration = section_variable_entry * strength
+type variable_declaration = dir_path * section_variable_entry * strength
 
-val declare_variable : identifier -> variable_declaration -> variable
+val declare_variable : variable -> variable_declaration -> section_path
 
 type constant_declaration_type =
   | ConstantEntry  of constant_entry
@@ -57,10 +59,6 @@ val declare_parameter : identifier -> constr -> constant
    the whole block *)
 val declare_mind : mutual_inductive_entry -> mutual_inductive
 
-(* [declare_eliminations sp] declares elimination schemes associated
-   to the mutual inductive block refered by [sp] *)
-val declare_eliminations : mutual_inductive -> unit
-
 val out_inductive : Libobject.obj -> mutual_inductive_entry 
 
 val make_strength_0 : unit -> strength
@@ -78,13 +76,12 @@ val get_variable : variable -> named_declaration * strength
 val get_variable_with_constraints : 
   variable -> named_declaration * Univ.constraints * strength
 val variable_strength : variable -> strength
-val find_section_variable : identifier -> variable
+val find_section_variable : variable -> section_path
 val last_section_hyps : dir_path -> identifier list
 
 (*s Global references *)
 
 val context_of_global_reference : global_reference -> section_context
-val extract_instance : global_reference -> constr array -> constr array
 
 (* Turn a global reference into a construction *)
 val constr_of_reference : global_reference -> constr
@@ -108,12 +105,3 @@ val global_reference : identifier -> constr
 val construct_reference : Environ.env -> identifier -> constr
 
 val is_global : identifier -> bool
-
-val path_of_inductive_path : inductive -> mutual_inductive
-val path_of_constructor_path : constructor -> mutual_inductive
-
-(* Look up function for the default elimination constant *)
-val elimination_suffix : sorts_family -> string
-val make_elimination_ident :
-  inductive_ident:identifier -> sorts_family -> identifier
-val lookup_eliminator : Environ.env -> inductive -> sorts_family -> constr
diff --git a/library/global.ml b/library/global.ml
index b55f741dd..3f009d6d2 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -11,7 +11,6 @@
 open Util
 open Names
 open Term
-open Instantiate
 open Sign
 open Environ
 open Safe_typing
@@ -35,69 +34,38 @@ let _ =
 
 (* Then we export the functions of [Typing] on that environment. *)
 
-let universes () = universes !global_env
-let context () = context !global_env
-let named_context () = named_context !global_env
-
-let push_named_def idc =
-  let d, env = check_and_push_named_def idc !global_env in
-  global_env := env; d
-
-let push_named_assum idc =
-  let d, env = check_and_push_named_assum idc !global_env in
-  global_env := env; d
+let universes () = universes (env())
+let named_context () = named_context (env())
+
+let push_named_assum a =
+  let (cst,env) = push_named_assum a !global_env in
+  global_env := env;
+  cst
+let push_named_def d =
+  let (cst,env) = push_named_def d !global_env in
+  global_env := env;
+  cst
+let pop_named_decls ids = global_env := pop_named_decls ids !global_env
 
-let add_parameter sp c l = global_env := add_parameter sp c l !global_env
-let add_constant sp ce l = global_env := add_constant sp ce l !global_env
-let add_discharged_constant sp r l = 
-  global_env := add_discharged_constant sp r l !global_env
-let add_mind sp mie l = global_env := add_mind sp mie l !global_env
+let add_parameter sp c = global_env := add_parameter sp c !global_env
+let add_constant sp ce = global_env := add_constant sp ce !global_env
+let add_discharged_constant sp r = 
+  global_env := add_discharged_constant sp r !global_env
+let add_mind sp mie = global_env := add_mind sp mie !global_env
 let add_constraints c = global_env := add_constraints c !global_env
 
-let pop_named_decls ids = global_env := pop_named_decls ids !global_env
-
-let lookup_named id = lookup_named id !global_env
-let lookup_constant sp = lookup_constant sp !global_env
-let lookup_mind sp = lookup_mind sp !global_env
-let lookup_mind_specif c = lookup_mind_specif c !global_env
+let lookup_named id = lookup_named id (env())
+let lookup_constant sp = lookup_constant sp (env())
+let lookup_inductive ind = Inductive.lookup_mind_specif (env()) ind
+let lookup_mind sp = lookup_mind sp (env())
 
 let export s = export !global_env s
 let import cenv = global_env := import cenv !global_env
 
-(* Some instanciations of functions from [Environ]. *)
-
-let sp_of_global ref = Environ.sp_of_global (env_of_safe_env !global_env) ref
-
-(* To know how qualified a name should be to be understood in the current env*)
-
-let qualid_of_global ref =  
-  let sp = sp_of_global ref in
-  let id = basename sp in
-  let rec find_visible dir qdir =
-    let qid = Nametab.make_qualid qdir id in
-    if (try Nametab.locate qid = ref with Not_found -> false) then qid
-    else match dir with
-      | [] -> Nametab.qualid_of_sp sp
-      | a::l -> find_visible l (add_dirpath_prefix a qdir)
-  in
-  find_visible (rev_repr_dirpath (dirpath sp)) (make_dirpath [])
-
-let string_of_global ref = Nametab.string_of_qualid (qualid_of_global ref)
-
 (*s Function to get an environment from the constants part of the global
     environment and a given context. *)
 
 let env_of_context hyps = 
-  change_hyps (fun _ -> hyps) (env_of_safe_env !global_env)
-
-(* Functions of [Inductive], composed with [lookup_mind_specif]. *)
-(* Rem:Cannot open Inductive to avoid clash with Inductive.lookup_mind_specif*)
-
-let mind_is_recursive =
-  Util.compose Inductive.mis_is_recursive lookup_mind_specif 
-
-let mind_nconstr = Util.compose Inductive.mis_nconstr lookup_mind_specif
-let mind_nparams = Util.compose Inductive.mis_nparams lookup_mind_specif
-let mind_nf_lc = Util.compose Inductive.mis_nf_lc lookup_mind_specif
+  reset_with_named_context hyps (env())
 
 
diff --git a/library/global.mli b/library/global.mli
index a9cda1289..0a5edc9ad 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -12,10 +12,8 @@
 open Names
 open Univ
 open Term
-open Sign
 open Declarations
-open Inductive
-open Environ
+open Indtypes
 open Safe_typing
 (*i*)
 
@@ -24,51 +22,34 @@ open Safe_typing
    operating on that global environment. *)
 
 val safe_env : unit -> safe_environment
-val env : unit -> env
+val env : unit -> Environ.env
 
 val universes : unit -> universes
-val context : unit -> context
-val named_context : unit -> named_context
+val named_context : unit -> Sign.named_context
 
-(* This has also a side-effect to push the declaration in the environment*)
-val push_named_assum : identifier * constr -> constr option * types*constraints
-val push_named_def : identifier * constr -> constr option * types * constraints
+(* Extending env with variables, constants and inductives *)
+val push_named_assum : (identifier * types) -> Univ.constraints
+val push_named_def   : (identifier * constr) -> Univ.constraints
+val pop_named_decls  : identifier list -> unit
 
-val add_parameter : section_path -> constr -> local_names -> unit
-val add_constant : section_path -> constant_entry -> local_names -> unit
-val add_discharged_constant : section_path -> Cooking.recipe -> 
-  local_names -> unit
-val add_mind : section_path -> mutual_inductive_entry -> local_names -> unit
-val add_constraints : constraints -> unit
-
-val pop_named_decls : identifier list -> unit
-
-val lookup_named : identifier -> constr option * types
-val lookup_constant : section_path -> constant_body
-val lookup_mind : section_path -> mutual_inductive_body
-val lookup_mind_specif : inductive -> inductive_instance
-
-val export : dir_path -> compiled_env
-val import : compiled_env -> unit
+val add_parameter           : constant -> types -> unit
+val add_constant            : constant -> constant_entry -> unit
+val add_discharged_constant : constant -> Cooking.recipe -> unit
 
-(*s Some functions of [Environ] instanciated on the global environment. *)
+val add_mind        : mutual_inductive -> mutual_inductive_entry -> unit
+val add_constraints : constraints -> unit
 
-val sp_of_global : global_reference -> section_path
+(* Queries *)
+val lookup_named     : variable -> named_declaration
+val lookup_constant  : constant -> constant_body
+val lookup_inductive : inductive -> mutual_inductive_body * one_inductive_body
+val lookup_mind      : mutual_inductive -> mutual_inductive_body
 
-(*s This is for printing purpose *)
-val qualid_of_global : global_reference -> Nametab.qualid
-val string_of_global : global_reference -> string
+(* Modules *)
+val export : dir_path -> Environ.compiled_env
+val import : Environ.compiled_env -> unit
 
 (*s Function to get an environment from the constants part of the global
     environment and a given context. *)
 
-val env_of_context : named_context -> env
-
-(*s Re-exported functions of [Inductive], composed with 
-    [lookup_mind_specif]. *)
-
-val mind_is_recursive : inductive -> bool
-val mind_nconstr : inductive -> int
-val mind_nparams : inductive -> int
-val mind_nf_lc : inductive -> constr array
-
+val env_of_context : Sign.named_context -> Environ.env
diff --git a/library/goptions.ml b/library/goptions.ml
index 9af867ce7..0eae518b4 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -15,6 +15,7 @@ open Util
 open Libobject
 open Names
 open Term
+open Nametab
 
 (****************************************************************************)
 (* 0- Common things                                                         *)
@@ -301,7 +302,7 @@ let msg_option_value (name,v) =
     | BoolValue false -> [< 'sTR "false" >]
     | IntValue n      -> [< 'iNT n >]
     | StringValue s   -> [< 'sTR s >]
-    | IdentValue id    -> [< 'sTR (Global.string_of_global id) >]
+    | IdentValue id    -> pr_sp(Nametab.sp_of_global (Global.env())id)
 
 let print_option_value key =
   let (name,(_,read,_)) = get_option key in
diff --git a/library/goptions.mli b/library/goptions.mli
index 92eeb4108..8f810a266 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -56,6 +56,7 @@
 open Pp
 open Names
 open Term
+open Nametab
 (*i*)
 
 (*s Things common to tables and options. *)
diff --git a/library/impargs.ml b/library/impargs.ml
index e203a594d..fec4df020 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -17,6 +17,7 @@ open Environ
 open Inductive
 open Libobject
 open Lib
+open Nametab
 
 (* calcul des arguments implicites *)
 
@@ -31,7 +32,7 @@ let ord_add x l =
     
 let add_free_rels_until bound m acc =
   let rec frec depth acc c = match kind_of_term c with
-    | IsRel n when (n < bound+depth) & (n >= depth) ->
+    | Rel n when (n < bound+depth) & (n >= depth) ->
 	Intset.add (bound+depth-n) acc
     | _ -> fold_constr_with_binders succ frec depth acc c
   in 
@@ -39,17 +40,17 @@ let add_free_rels_until bound m acc =
 
 (* calcule la liste des arguments implicites *)
 
-let compute_implicits env sigma t =
+let compute_implicits env t =
   let rec aux env n t =
-    match kind_of_term (whd_betadeltaiota env sigma t) with
-      | IsProd (x,a,b) ->
+    match kind_of_term (whd_betadeltaiota env t) with
+      | Prod (x,a,b) ->
 	  add_free_rels_until n a
-	    (aux (push_rel_assum (x,a) env) (n+1) b)
+	    (aux (push_rel (x,None,a) env) (n+1) b)
       | _ -> Intset.empty
   in 
-  match kind_of_term (whd_betadeltaiota env sigma t) with 
-    | IsProd (x,a,b) ->
-	Intset.elements (aux (push_rel_assum (x,a) env) 1 b)
+  match kind_of_term (whd_betadeltaiota env t) with 
+    | Prod (x,a,b) ->
+	Intset.elements (aux (push_rel (x,None,a) env) 1 b)
     | _ -> []
 
 type implicits_list = int list
@@ -82,7 +83,7 @@ let using_implicits = function
   | No_impl -> with_implicits false
   | _ -> with_implicits true
 
-let auto_implicits env ty = Impl_auto (compute_implicits env Evd.empty ty)
+let auto_implicits env ty = Impl_auto (compute_implicits env ty)
 
 let list_of_implicits = function 
   | Impl_auto l -> l
@@ -128,7 +129,7 @@ let constant_implicits_list sp =
 module Inductive_path = struct
   type t = inductive
   let compare (spx,ix) (spy,iy) = 
-    let c = ix - iy in if c = 0 then sp_ord spx spy else c
+    let c = ix - iy in if c = 0 then compare spx spy else c
 end
 
 module Indmap = Map.Make(Inductive_path)
@@ -174,11 +175,16 @@ let (in_constructor_implicits, _) =
 let compute_mib_implicits sp =
   let env = Global.env () in
   let mib = lookup_mind sp env in
-  let env_ar = push_rels (mind_arities_context mib) env in
+  let ar =
+    Array.to_list
+      (Array.map  (* No need to lift, arities contain no de Bruijn *)
+        (fun mip -> (Name mip.mind_typename, None, mip.mind_user_arity))
+        mib.mind_packets) in
+  let env_ar = push_rel_context ar env in
   let imps_one_inductive mip =
-    (auto_implicits env (body_of_type (mind_user_arity mip)),
+    (auto_implicits env (body_of_type mip.mind_user_arity),
      Array.map (fun c -> auto_implicits env_ar (body_of_type c))
-       (mind_user_lc mip))
+       mip.mind_user_lc)
   in
   Array.map imps_one_inductive mib.mind_packets
 
@@ -220,15 +226,15 @@ let inductive_implicits_list ind_sp =
 
 (*s Variables. *)
 
-let var_table = ref Spmap.empty
+let var_table = ref Idmap.empty
 
-let compute_var_implicits sp =
+let compute_var_implicits id =
   let env = Global.env () in
-  let (_,ty) = lookup_named (basename sp) env in
+  let (_,_,ty) = lookup_named id env in
   auto_implicits env (body_of_type ty)
 
-let cache_var_implicits (_,(sp,imps)) =
-  var_table := Spmap.add sp imps !var_table
+let cache_var_implicits (_,(id,imps)) =
+  var_table := Idmap.add id imps !var_table
 
 let (in_var_implicits, _) =
   let od = {
@@ -239,12 +245,12 @@ let (in_var_implicits, _) =
   in
   declare_object ("VARIABLE-IMPLICITS", od)
 
-let declare_var_implicits sp =
-  let imps = compute_var_implicits sp in
-  add_anonymous_leaf (in_var_implicits (sp,imps))
+let declare_var_implicits id =
+  let imps = compute_var_implicits id in
+  add_anonymous_leaf (in_var_implicits (id,imps))
 
-let implicits_of_var sp =
-  list_of_implicits (try Spmap.find sp !var_table with Not_found -> No_impl)
+let implicits_of_var id =
+  list_of_implicits (try Idmap.find id !var_table with Not_found -> No_impl)
 
 (*s Implicits of a global reference. *)
 
@@ -270,27 +276,28 @@ let context_of_global_reference = function
 
 let type_of_global r =
   match r with
-  | VarRef sp ->
-      lookup_named_type (basename sp) (Global.env ())
+  | VarRef id ->
+      let (_,_,ty) = lookup_named id (Global.env ()) in
+      ty
   | ConstRef sp ->
-      Typeops.type_of_constant (Global.env ()) Evd.empty sp
+      Environ.constant_type (Global.env ()) sp
   | IndRef sp -> 
-      Typeops.type_of_inductive (Global.env ()) Evd.empty sp
+      Inductive.type_of_inductive (Global.env ()) sp
   | ConstructRef sp ->
-      Typeops.type_of_constructor (Global.env ()) Evd.empty sp
+      Inductive.type_of_constructor (Global.env ()) sp
 
 let check_range n i =
   if i<1 or i>n then error ("Bad argument number: "^(string_of_int i))
 
 let declare_manual_implicits r l =
   let t = type_of_global r in
-  let n = List.length (fst (splay_prod (Global.env()) Evd.empty t)) in
+  let n = List.length (fst (dest_prod (Global.env()) t)) in
   if not (list_distinct l) then error ("Some numbers occur several time");
   List.iter (check_range n) l;
   let l = List.sort (-) l in
   match r with
-  | VarRef sp -> 
-      add_anonymous_leaf (in_var_implicits (sp,Impl_manual l))
+  | VarRef id -> 
+      add_anonymous_leaf (in_var_implicits (id,Impl_manual l))
   | ConstRef sp ->
       add_anonymous_leaf (in_constant_implicits (sp,Impl_manual l))
   | IndRef indp ->
@@ -307,11 +314,11 @@ let is_implicit_inductive_definition indp =
   try let _ = Indmap.find indp !inductives_table in true 
   with Not_found -> false
 
-let is_implicit_var sp =
-  try let _ = Spmap.find sp !var_table in true with Not_found -> false
+let is_implicit_var id =
+  try let _ = Idmap.find id !var_table in true with Not_found -> false
 
 let implicits_of_global = function
-  | VarRef sp -> implicits_of_var sp
+  | VarRef id -> implicits_of_var id
   | ConstRef sp -> list_of_implicits (constant_implicits sp)
   | IndRef isp -> list_of_implicits (inductive_implicits isp)
   | ConstructRef csp ->	list_of_implicits (constructor_implicits csp)
@@ -321,13 +328,13 @@ let implicits_of_global = function
 type frozen_t = implicits Spmap.t 
               * implicits Indmap.t 
 	      * implicits Constrmap.t
-              * implicits Spmap.t
+              * implicits Idmap.t
 
 let init () =
   constants_table := Spmap.empty;
   inductives_table := Indmap.empty;
   constructors_table := Constrmap.empty;
-  var_table := Spmap.empty
+  var_table := Idmap.empty
 
 let freeze () =
   (!constants_table, !inductives_table, 
diff --git a/library/impargs.mli b/library/impargs.mli
index ceaa30cdf..46d03d996 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -13,6 +13,7 @@ open Names
 open Term
 open Environ
 open Inductive
+open Nametab
 (*i*)
 
 (*s Implicit arguments. Here we store the implicit arguments. Notice that we 
@@ -29,7 +30,7 @@ type implicits_list = int list
 
 (* Computation of the positions of arguments automatically inferable
    for an object of the given type in the given env *)
-val compute_implicits : env -> 'a Evd.evar_map -> types -> implicits_list
+val compute_implicits : env -> types -> implicits_list
 
 (*s Computation of implicits (done using the global environment). *)
 
diff --git a/library/indrec.ml b/library/indrec.ml
deleted file mode 100644
index 36ce4f783..000000000
--- a/library/indrec.ml
+++ /dev/null
@@ -1,501 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$ *)
-
-open Pp
-open Util
-open Names
-open Term
-open Declarations
-open Inductive
-open Instantiate
-open Environ
-open Reduction
-open Typeops
-open Type_errors
-open Indtypes (* pour les erreurs *)
-
-let make_prod_dep dep env = if dep then prod_name env else mkProd
-
-(*******************************************)
-(* Building curryfied elimination          *)
-(*******************************************)
-
-(**********************************************************************)
-(* Building case analysis schemes *)
-(* Nouvelle version, plus concise mais plus coûteuse à cause de
-   lift_constructor et lift_inductive_family qui ne se contentent pas de 
-   lifter les paramètres globaux *)
-
-let mis_make_case_com depopt env sigma mispec kind =
-  let lnamespar = mis_params_ctxt mispec in
-  let nparams = mis_nparams mispec in
-  let dep = match depopt with 
-    | None -> mis_sort mispec <> (Prop Null)
-    | Some d -> d
-  in
-  if not (List.exists ((=) kind) (mis_kelim mispec)) then
-    raise
-      (InductiveError
-	 (NotAllowedCaseAnalysis
-	    (dep,(new_sort_in_family kind),mis_inductive mispec)));
-
-  let nbargsprod = mis_nrealargs mispec + 1 in
-
-  (* Pas génant car env ne sert pas à typer mais juste à renommer les Anonym *)
-  (* mais pas très joli ... (mais manque get_sort_of à ce niveau) *)
-  let env' = push_rels lnamespar env in
-
-  let indf = make_ind_family (mispec, extended_rel_list 0 lnamespar) in
-  let constrs = get_constructors indf in
-
-  let rec add_branch env k = 
-    if k = mis_nconstr mispec then
-      let nbprod = k+1 in
-      let indf = make_ind_family (mispec,extended_rel_list nbprod lnamespar) in
-      let lnamesar,_ = get_arity indf in
-      let ci = make_default_case_info mispec in
-      it_mkLambda_or_LetIn_name env'
-       	(lambda_create env'
-           (build_dependent_inductive indf,
-            mkMutCase (ci,
-		       mkRel (nbprod+nbargsprod),
-		       mkRel 1,
-		       rel_vect nbargsprod k)))
-       	lnamesar
-    else
-      let cs = lift_constructor (k+1) constrs.(k) in
-      let t = build_branch_type env dep (mkRel (k+1)) cs in
-      mkLambda_string "f" t
-	(add_branch (push_rel (Anonymous, None, t) env) (k+1))
-  in
-  let typP = make_arity env' dep indf (new_sort_in_family kind) in
-  it_mkLambda_or_LetIn_name env 
-    (mkLambda_string "P" typP
-       (add_branch (push_rel (Anonymous,None,typP) env') 0)) lnamespar
-    
-(* check if the type depends recursively on one of the inductive scheme *)
-
-(**********************************************************************)
-(* Building the recursive elimination *)
-
-(*
- * t is the type of the constructor co and recargs is the information on 
- * the recursive calls. (It is assumed to be in form given by the user).
- * build the type of the corresponding branch of the recurrence principle
- * assuming f has this type, branch_rec gives also the term 
- *   [x1]..[xk](f xi (F xi) ...) to be put in the corresponding branch of 
- * the case operation
- * FPvect gives for each inductive definition if we want an elimination 
- * on it with which predicate and which recursive function. 
- *)
-
-let type_rec_branch dep env sigma (vargs,depPvect,decP) tyi cs recargs = 
-  let make_prod = make_prod_dep dep in
-  let nparams = List.length vargs in
-  let process_pos env depK pk =
-    let rec prec env i sign p =
-      let p',largs = whd_betadeltaiota_nolet_stack env sigma p in
-      match kind_of_term p' with
-	| IsProd (n,t,c) ->
-	    let d = (n,None,t) in
-	    make_prod env (n,t,prec (push_rel d env) (i+1) (d::sign) c)
-	| IsLetIn (n,b,t,c) ->
-	    let d = (n,Some b,t) in
-	    mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::sign) c)
-     	| IsMutInd (_,_) ->
-	    let (_,realargs) = list_chop nparams largs in
-	    let base = applist (lift i pk,realargs) in
-            if depK then 
-	      mkApp (base, [|applist (mkRel (i+1),extended_rel_list 0 sign)|])
-            else 
-	      base
-      	| _ -> assert false 
-    in
-    prec env 0 []
-  in
-  let rec process_constr env i c recargs nhyps li =
-    if nhyps > 0 then match kind_of_term c with 
-      | IsProd (n,t,c_0) ->
-          let (optionpos,rest) = 
-	    match recargs with 
-	      | [] -> None,[] 
-	      | Param _ :: rest -> (None,rest)
-	      | Norec :: rest   -> (None,rest)
-	      | Imbr _ :: rest  -> 
-		  warning "Ignoring recursive call"; (None,rest) 
-	      | Mrec j :: rest -> (depPvect.(j),rest)
-	  in 
-          (match optionpos with 
-	     | None -> 
-		 make_prod env
-		   (n,t,
-		    process_constr (push_rel (n,None,t) env) (i+1) c_0 rest
-		      (nhyps-1) (i::li))
-             | Some(dep',p) -> 
-		 let nP = lift (i+1+decP) p in
-		 let t_0 = process_pos env dep' nP (lift 1 t) in 
-		 make_prod_dep (dep or dep') env
-                   (n,t,
-		    mkArrow t_0
-		      (process_constr
-			 (push_rel (n,None,t)
-			    (push_rel (Anonymous,None,t_0) env))
-			 (i+2) (lift 1 c_0) rest (nhyps-1) (i::li))))
-      | IsLetIn (n,b,t,c_0) ->
-	  mkLetIn (n,b,t,
-		   process_constr
-		     (push_rel (n,Some b,t) env)
-		     (i+1) c_0 recargs (nhyps-1) li)
-      | _ -> assert false
-    else
-      if dep then
-	let realargs = List.map (fun k -> mkRel (i-k)) (List.rev li) in
-        let params = List.map (lift i) vargs in
-        let co = applist (mkMutConstruct cs.cs_cstr,params@realargs) in
-	mkApp (c, [|co|])
-      else c
-(*
-    let c', largs = whd_stack c in
-    match kind_of_term c' with 
-      | IsProd (n,t,c_0) ->
-          let (optionpos,rest) = 
-	    match recargs with 
-	      | [] -> None,[] 
-	      | Param _ :: rest -> (None,rest)
-	      | Norec :: rest   -> (None,rest)
-	      | Imbr _ :: rest  -> 
-		  warning "Ignoring recursive call"; (None,rest) 
-	      | Mrec j :: rest -> (depPvect.(j),rest)
-	  in 
-          (match optionpos with 
-	     | None -> 
-		 make_prod env
-		   (n,t,
-		    process_constr (push_rel (n,None,t) env) (i+1) c_0 rest 
-		      (mkApp (lift 1 co, [|mkRel 1|])))
-             | Some(dep',p) -> 
-		 let nP = lift (i+1+decP) p in
-		 let t_0 = process_pos env dep' nP (lift 1 t) in 
-		 make_prod_dep (dep or dep') env
-                   (n,t,
-		    mkArrow t_0
-		      (process_constr
-			 (push_rel (n,None,t)
-			    (push_rel (Anonymous,None,t_0) env))
-			 (i+2) (lift 1 c_0) rest
-			 (mkApp (lift 2 co, [|mkRel 2|])))))
-      | IsLetIn (n,b,t,c_0) ->
-	  mkLetIn (n,b,t,
-		   process_constr
-		     (push_rel (n,Some b,t) env)
-		     (i+1) c_0 recargs (lift 1 co))
-
-      | IsMutInd ((_,tyi),_) -> 
-      	  let nP = match depPvect.(tyi) with 
-	    | Some(_,p) -> lift (i+decP) p
-	    | _ -> assert false in
-      	  let (_,realargs) = list_chop nparams largs in
-      	  let base = applist (nP,realargs) in
-          if dep then mkApp (base, [|co|]) else base
-      | _ -> assert false
-*)
-  in
-  let nhyps = List.length cs.cs_args in
-  let nP = match depPvect.(tyi) with 
-    | Some(_,p) -> lift (nhyps+decP) p
-    | _ -> assert false in
-  let base = appvect (nP,cs.cs_concl_realargs) in
-  let c = it_mkProd_or_LetIn base cs.cs_args in
-  process_constr env 0 c recargs nhyps []
-
-let make_rec_branch_arg env sigma (nparams,fvect,decF) f cstr recargs = 
-  let process_pos env fk  =
-    let rec prec env i hyps p =
-      let p',largs = whd_betadeltaiota_nolet_stack env sigma p in
-      match kind_of_term p' with
-	| IsProd (n,t,c) ->
-	    let d = (n,None,t) in
-	    lambda_name env (n,t,prec (push_rel d env) (i+1) (d::hyps) c)
-	| IsLetIn (n,b,t,c) ->
-	    let d = (n,Some b,t) in
-	    mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c)
-     	| IsMutInd _ -> 
-            let (_,realargs) = list_chop nparams largs
-            and arg = appvect (mkRel (i+1),extended_rel_vect 0 hyps) in 
-            applist(lift i fk,realargs@[arg])
-     	| _ -> assert false
-    in
-    prec env 0 []
-  in
-  (* ici, cstrprods est la liste des produits du constructeur instantié *)
-  let rec process_constr env i f = function
-    | (n,None,t as d)::cprest, recarg::rest -> 
-        let optionpos = 
-	  match recarg with 
-            | Param i -> None
-            | Norec   -> None
-            | Imbr _  -> None
-            | Mrec i  -> fvect.(i)
-	in 
-        (match optionpos with 
-           | None ->
-	       lambda_name env
-		 (n,t,process_constr (push_rel d env) (i+1)
-		    (whd_beta (applist (lift 1 f, [(mkRel 1)])))
-		    (cprest,rest))
-           | Some(_,f_0) -> 
-	       let nF = lift (i+1+decF) f_0 in
-	       let arg = process_pos env nF (lift 1 (body_of_type t)) in 
-               lambda_name env
-		 (n,t,process_constr (push_rel d env) (i+1)
-		    (whd_beta (applist (lift 1 f, [(mkRel 1); arg])))
-		    (cprest,rest)))
-    | (n,Some c,t as d)::cprest, rest ->
-	mkLetIn
-	  (n,c,t,
-	   process_constr (push_rel d env) (i+1) (lift 1 f)
-	     (cprest,rest))
-    | [],[] -> f
-    | _,[] | [],_ -> anomaly "process_constr"
-
-  in
-  process_constr env 0 f (List.rev cstr.cs_args, recargs)
-
-(* Main function *)
-let mis_make_indrec env sigma listdepkind mispec =
-  let nparams = mis_nparams mispec in
-  let lnamespar = mis_params_ctxt mispec in
-  let env' =  (* push_rels lnamespar *) env in
-  let nrec = List.length listdepkind in
-  let depPvec =
-    Array.create (mis_ntypes mispec) (None : (bool * constr) option) in 
-  let _ = 
-    let rec 
-      assign k = function 
-	| [] -> ()
-        | (mispeci,dep,_)::rest -> 
-            (Array.set depPvec (mis_index mispeci) (Some(dep,mkRel k));
-             assign (k-1) rest)
-    in 
-    assign nrec listdepkind  
-  in 
-  let recargsvec = mis_recargs mispec in
-  let make_one_rec p =
-    let makefix nbconstruct =
-      let rec mrec i ln ltyp ldef = function
-	| (mispeci,dep,_)::rest ->
-	    let tyi = mis_index mispeci in
-	    let nctyi = mis_nconstr mispeci in (* nb constructeurs du type *) 
-
-            (* arity in the context P1..P_nrec f1..f_nbconstruct *)
-	    let args = extended_rel_list (nrec+nbconstruct) lnamespar in
-	    let indf = make_ind_family (mispeci,args) in
-	    let lnames,_ = get_arity indf in
-
-	    let nar = mis_nrealargs mispeci in
-	    let decf = nar+nrec+nbconstruct+nrec in 
-	    let dect = nar+nrec+nbconstruct in
-	    let vecfi = rel_vect (dect+1-i-nctyi) nctyi in
-
-	    let args = extended_rel_list (decf+1) lnamespar in
-	    let constrs = get_constructors (make_ind_family (mispeci,args)) in
-	    let branches = 
-	      array_map3
-		(make_rec_branch_arg env sigma (nparams,depPvec,nar+1))
-                vecfi constrs recargsvec.(tyi) in
-	    let j = (match depPvec.(tyi) with 
-		       | Some (_,c) when isRel c -> destRel c 
-		       | _ -> assert false) in
-	    let args = extended_rel_list (nrec+nbconstruct) lnamespar in
-	    let indf = make_ind_family (mispeci,args) in
-	    let deftyi = 
-	      it_mkLambda_or_LetIn_name env
-		(lambda_create env
-		   (build_dependent_inductive
-                     (lift_inductive_family nrec indf),
-		    mkMutCase (make_default_case_info mispeci,
-			       mkRel (dect+j+1), mkRel 1, branches)))
-		(Sign.lift_rel_context nrec lnames)
-	    in
-	    let ind = build_dependent_inductive indf in
-	    let typtyi = 
-	      it_mkProd_or_LetIn_name env
-		(prod_create env
-		   (ind,
-		    (if dep then 
-		       let ext_lnames = (Anonymous,None,ind)::lnames in
-		       let args = extended_rel_list 0 ext_lnames in
-		       applist (mkRel (nbconstruct+nar+j+1), args)
-		     else
-		       let args = extended_rel_list 1 lnames in
-		       applist (mkRel (nbconstruct+nar+j+1), args))))
-          	lnames
-	    in 
-	    mrec (i+nctyi) (nar::ln) (typtyi::ltyp) (deftyi::ldef) rest
-        | [] -> 
-	    let fixn = Array.of_list (List.rev ln) in
-            let fixtyi = Array.of_list (List.rev ltyp) in
-            let fixdef = Array.of_list (List.rev ldef) in 
-            let names = Array.create nrec (Name(id_of_string "F")) in
-	    mkFix ((fixn,p),(names,fixtyi,fixdef))
-      in 
-      mrec 0 [] [] [] 
-    in 
-    let rec make_branch env i = function 
-      | (mispeci,dep,_)::rest ->
-          let tyi = mis_index mispeci in
-	  let nconstr = mis_nconstr mispeci in
-	  let rec onerec env j = 
-	    if j = nconstr then 
-	      make_branch env (i+j) rest 
-	    else 
-	      let recarg = recargsvec.(tyi).(j) in
-	      let vargs = extended_rel_list (nrec+i+j) lnamespar in
-	      let indf = make_ind_family (mispeci, vargs) in
-	      let cs = get_constructor indf (j+1) in
-	      let p_0 =
-		type_rec_branch dep env sigma (vargs,depPvec,i+j) tyi cs recarg
-	      in 
-	      mkLambda_string "f" p_0
-		(onerec (push_rel (Anonymous,None,p_0) env) (j+1))
-	  in onerec env 0
-      | [] -> 
-	  makefix i listdepkind
-    in 
-    let rec put_arity env i = function 
-      | (mispeci,dep,kinds)::rest -> 
-	  let indf = make_ind_family (mispeci,extended_rel_list i lnamespar) in
-	  let typP = make_arity env dep indf (new_sort_in_family kinds) in
-	  mkLambda_string "P" typP
-	    (put_arity (push_rel (Anonymous,None,typP) env) (i+1) rest)
-      | [] -> 
-	  make_branch env 0 listdepkind 
-    in 
-    let (mispeci,dep,kind) = List.nth listdepkind p in
-    let env' = push_rels lnamespar env in
-    if mis_is_recursive_subset
-      (List.map (fun (mispec,_,_) -> mis_index mispec) listdepkind) mispeci
-    then 
-      it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind) lnamespar
-    else 
-      mis_make_case_com (Some dep) env sigma mispeci kind 
-  in 
-  list_tabulate make_one_rec nrec
-
-(**********************************************************************)
-(* This builds elimination predicate for Case tactic *)
-
-let make_case_com depopt env sigma ity kind =
-  let mispec = lookup_mind_specif ity env in 
-  mis_make_case_com depopt env sigma mispec kind
-
-let make_case_dep env   = make_case_com (Some true) env
-let make_case_nodep env = make_case_com (Some false) env 
-let make_case_gen env   = make_case_com None env
-
-
-(**********************************************************************)
-(* [instanciate_indrec_scheme s rec] replace the sort of the scheme
-   [rec] by [s] *)
-
-let change_sort_arity sort = 
-  let rec drec a = match kind_of_term a with
-    | IsCast (c,t) -> drec c 
-    | IsProd (n,t,c) -> mkProd (n, t, drec c)
-    | IsSort _ -> mkSort sort
-    | _ -> assert false
-  in 
-  drec 
-
-(* [npar] is the number of expected arguments (then excluding letin's) *)
-let instanciate_indrec_scheme sort =
-  let rec drec npar elim =
-    match kind_of_term elim with
-      | IsLambda (n,t,c) -> 
-	  if npar = 0 then 
-	    mkLambda (n, change_sort_arity sort t, c)
-	  else 
-	    mkLambda (n, t, drec (npar-1) c)
-      | IsLetIn (n,b,t,c) -> mkLetIn (n,b,t,drec npar c)
-      | _ -> anomaly "instanciate_indrec_scheme: wrong elimination type"
-  in
-  drec
-
-(**********************************************************************)
-(* Interface to build complex Scheme *)
-
-let check_arities listdepkind = 
-  List.iter 
-    (function (mispeci,dep,kind) -> 
-       let id = mis_typename mispeci  in
-       let kelim = mis_kelim mispeci in
-       if not (List.exists ((=) kind) kelim) then
-	 raise
-	   (InductiveError (BadInduction (dep, id, new_sort_in_family kind))))
-    listdepkind
-
-let build_mutual_indrec env sigma = function 
-  | (mind,dep,s)::lrecspec ->
-      let (sp,tyi) = mind in
-      let mispec = lookup_mind_specif mind env in
-      let listdepkind = 
-    	(mispec, dep,s)::
-    	(List.map
-	   (function (mind',dep',s') ->
-	      let (sp',_) = mind' in
-	      if sp=sp' then 
-		(lookup_mind_specif mind' env,dep',s') 
-	      else 
-		raise (InductiveError NotMutualInScheme))
-	   lrecspec)
-      in
-      let _ = check_arities listdepkind in 
-      mis_make_indrec env sigma listdepkind mispec
-  | _ -> anomaly "build_indrec expects a non empty list of inductive types"
-
-let build_indrec env sigma mispec =
-  let kind = family_of_sort (mis_sort mispec) in
-  let dep = kind <> InProp in
-  List.hd (mis_make_indrec env sigma [(mispec,dep,kind)] mispec)
-
-(**********************************************************************)
-(* To handle old Case/Match syntax in Pretyping                       *)
-
-(***********************************)
-(* To interpret the Match operator *)
-
-(* TODO: check that we can drop universe constraints ? *)
-let type_mutind_rec env sigma (IndType (indf,realargs) as ind) pj c = 
-  let p = pj.uj_val in
-  let (mispec,params) = dest_ind_family indf in
-  let tyi = mis_index mispec in
-  if mis_is_recursive_subset [tyi] mispec then
-    let (dep,_) = find_case_dep_nparams env sigma (c,pj) indf in 
-    let init_depPvec i = if i = tyi then Some(dep,p) else None in
-    let depPvec = Array.init (mis_ntypes mispec) init_depPvec in
-    let vargs = Array.of_list params in
-    let constructors = get_constructors indf in
-    let recargs = mis_recarg mispec in
-    let lft = array_map2 (type_rec_branch dep env sigma (params,depPvec,0) tyi)
-                constructors recargs in
-    (lft,
-     if dep then applist(p,realargs@[c]) 
-     else applist(p,realargs) )
-  else 
-    let (p,ra,_) = type_case_branches env sigma ind pj c in
-    (p,ra)
-
-let type_rec_branches recursive env sigma ind pj c =
-  if recursive then 
-    type_mutind_rec env sigma ind pj c
-  else 
-    let (p,ra,_) = type_case_branches env sigma ind pj c in
-    (p,ra)
-
diff --git a/library/indrec.mli b/library/indrec.mli
deleted file mode 100644
index aa3a0b6f1..000000000
--- a/library/indrec.mli
+++ /dev/null
@@ -1,47 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(*i $Id$ i*)
-
-(*i*)
-open Names
-open Term
-open Declarations
-open Inductive
-open Environ
-open Evd
-(*i*)
-
-(* Eliminations. *)
-
-(* These functions build elimination predicate for Case tactic *)
-
-val make_case_dep : env -> 'a evar_map -> inductive -> sorts_family -> constr
-val make_case_nodep : env -> 'a evar_map -> inductive -> sorts_family -> constr
-val make_case_gen : env -> 'a evar_map -> inductive -> sorts_family -> constr
-
-(* This builds an elimination scheme associated (using the own arity
-   of the inductive) *)
-
-val build_indrec : env -> 'a evar_map -> inductive_instance -> constr
-val instanciate_indrec_scheme : sorts -> int -> constr -> constr
-
-(* This builds complex [Scheme] *)
-
-val build_mutual_indrec : 
-  env -> 'a evar_map -> (inductive * bool * sorts_family) list
-    -> constr list
-
-(* These are for old Case/Match typing *)
-
-val type_rec_branches : bool -> env -> 'c evar_map -> inductive_type
-  -> unsafe_judgment -> constr -> constr array * constr
-val make_rec_branch_arg : 
-  env -> 'a evar_map ->
-    int * ('b * constr) option array * int ->
-    constr -> constructor_summary -> recarg list -> constr
diff --git a/library/lib.ml b/library/lib.ml
index e85e834ec..cd71de3a3 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -11,9 +11,11 @@
 open Pp
 open Util
 open Names
+open Nameops
 open Libobject
 open Summary
 
+
 type node = 
   | Leaf of obj
   | Module of dir_path
@@ -36,7 +38,6 @@ and library_segment = library_entry list
 
 let lib_stk = ref ([] : (section_path * node) list)
 
-let init_toplevel_root () = Nametab.push_library_root default_module
 
 let module_name = ref None
 let path_prefix = ref (default_module : dir_path)
@@ -54,11 +55,11 @@ let recalc_path_prefix () =
 
 let pop_path_prefix () = path_prefix := fst (split_dirpath !path_prefix)
 
-let make_path id k = Names.make_path !path_prefix id k
+let make_path id = Names.make_path !path_prefix id
 
 let sections_depth () =
-  List.length (rev_repr_dirpath !path_prefix)
-  - List.length (rev_repr_dirpath (module_sp ()))
+  List.length (repr_dirpath !path_prefix)
+  - List.length (repr_dirpath (module_sp ()))
 
 let cwd () = !path_prefix
 
@@ -87,7 +88,7 @@ let anonymous_id =
   fun () -> incr n; id_of_string ("_" ^ (string_of_int !n))
 
 let add_anonymous_entry node =
-  let sp = make_path (anonymous_id()) OBJ in
+  let sp = make_path (anonymous_id()) in
   add_entry sp node;
   sp
 
@@ -95,14 +96,14 @@ let add_absolutely_named_lead sp obj =
   cache_object (sp,obj);
   add_entry sp (Leaf obj)
 
-let add_leaf id kind obj =
-  let sp = make_path id kind in
+let add_leaf id obj =
+  let sp = make_path id in
   cache_object (sp,obj);
   add_entry sp (Leaf obj);
   sp
 
 let add_anonymous_leaf obj =
-  let sp = make_path (anonymous_id()) OBJ in
+  let sp = make_path (anonymous_id()) in
   cache_object (sp,obj);
   add_entry sp (Leaf obj)
 
@@ -117,7 +118,7 @@ let contents_after = function
 
 let open_section id =
   let dir = extend_dirpath !path_prefix id in
-  let sp = make_path id OBJ in
+  let sp = make_path id in
   if Nametab.exists_section dir then
     errorlabstrm "open_section" [< pr_id id; 'sTR " already exists" >];
   add_entry sp (OpenedSection (dir, freeze_summaries()));
@@ -139,7 +140,6 @@ let start_module s =
   if !path_prefix <> default_module then
     error "some sections are already opened";
   module_name := Some s;
-  Nametab.push_library_root s;
   Univ.set_module s;
   let _ = add_anonymous_entry (Module s) in
   path_prefix := s
@@ -148,7 +148,7 @@ let end_module s =
   match !module_name with
     | None -> error "no module declared"
     | Some m ->
-	let bm = snd (split_dirpath m) in
+        let (_,bm) = split_dirpath m in
 	if bm <> s then
 	  error ("The current open module has basename "^(string_of_id bm));
 	m
@@ -187,7 +187,7 @@ let close_section export id =
   lib_stk := before;
   let after' = export_segment after in
   pop_path_prefix ();
-  add_entry (make_path id OBJ) (ClosedSection (export, dir, after'));
+  add_entry (make_path id) (ClosedSection (export, dir, after'));
   (dir,after,fs)
 
 (* The following function exports the whole library segment, that will be 
@@ -222,7 +222,7 @@ let reset_to sp =
 let reset_name id =
   let (sp,_) = 
     try
-      find_entry_p (fun (sp,_) -> id = basename sp)
+      find_entry_p (fun (sp,_) -> let (_,spi) = repr_path sp in id = spi)
     with Not_found ->
       error (string_of_id id ^ ": no such entry")
   in
diff --git a/library/lib.mli b/library/lib.mli
index faf80428a..832e6cff9 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -33,7 +33,7 @@ and library_segment = library_entry list
 (*s Adding operations (which calls the [cache] method, and getting the
   current list of operations (most recent ones coming first). *)
 
-val add_leaf : identifier -> path_kind -> obj -> section_path
+val add_leaf : identifier -> obj -> section_path
 val add_absolutely_named_lead : section_path -> obj -> unit
 val add_anonymous_leaf : obj -> unit
 val add_frozen_state : unit -> unit
@@ -53,14 +53,11 @@ val close_section :
   export:bool -> identifier -> dir_path * library_segment * Summary.frozen
 val sections_are_opened : unit -> bool
 
-val make_path : identifier -> path_kind -> section_path
+val make_path : identifier -> section_path
 val cwd : unit -> dir_path
 val sections_depth : unit -> int
 val is_section_p : dir_path -> bool
 
-(* This is to declare the interactive toplevel default module name as a root*)
-val init_toplevel_root : unit -> unit
-
 val start_module : dir_path -> unit
 val end_module : module_ident -> dir_path
 val export_module : dir_path -> library_segment
diff --git a/library/library.ml b/library/library.ml
index 46c6b8b50..b35f7bbee 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -12,6 +12,7 @@ open Pp
 open Util
 
 open Names
+open Nameops
 open Environ
 open Libobject
 open Lib
@@ -57,7 +58,7 @@ let find_logical_path phys_dir =
   let phys_dir = canonical_path_name phys_dir in
   match list_filter2 (fun p d -> p = phys_dir) !load_path with
   | _,[dir] -> dir
-  | _,[] -> Nametab.default_root_prefix
+  | _,[] -> Nameops.default_root_prefix
   | _,l -> anomaly ("Two logical paths are associated to "^phys_dir)
 
 let remove_path dir =
@@ -71,11 +72,11 @@ let add_load_path_entry (phys_path,coq_path) =
         (* If this is not the default -I . to coqtop *)
         && not
         (phys_path = canonical_path_name Filename.current_dir_name
-         && coq_path = Nametab.default_root_prefix)
+         && coq_path = Nameops.default_root_prefix)
       then
 	begin
           (* Assume the user is concerned by module naming *)
-	  if dir <> Nametab.default_root_prefix then
+	  if dir <> Nameops.default_root_prefix then
 	    (Options.if_verbose warning (phys_path^" was previously bound to "
 	    ^(string_of_dirpath dir)
 	    ^("\nIt is remapped to "^(string_of_dirpath coq_path)));
@@ -264,7 +265,6 @@ let rec load_module = function
 	  [< 'sTR ("The file " ^ f ^ " contains module"); 'sPC;
 	  pr_dirpath md.md_name; 'sPC; 'sTR "and not module"; 'sPC;
 	  pr_dirpath dir >];
-      Nametab.push_library_root dir;
       compunit_cache := Stringmap.add f (md, digest) !compunit_cache;
       (md, digest) in
     intern_module digest f md
@@ -316,7 +316,7 @@ let locate_qualified_library qid =
   try
     let dir, base = repr_qualid qid in 
     let loadpath =
-      if is_empty_dirpath dir then get_load_path ()
+      if repr_dirpath dir = [] then get_load_path ()
       else 
         (* we assume dir is an absolute dirpath *)
 	load_path_of_logical_path dir
@@ -364,7 +364,6 @@ let locate_by_filename_only id f =
        m.module_filename);
     (LibLoaded, md.md_name, m.module_filename)
   with Not_found ->
-    Nametab.push_library_root md.md_name;
     compunit_cache := Stringmap.add f (md, digest) !compunit_cache;
     (LibInPath, md.md_name, f)
 
@@ -372,7 +371,7 @@ let locate_module qid = function
   | Some f ->
       (* A name is specified, we have to check it contains module id *)
       let prefix, id = repr_qualid qid in
-      assert (is_empty_dirpath prefix);
+      assert (repr_dirpath prefix = []);
       let _, f = System.find_file_in_path (get_load_path ()) (f^".vo") in
       locate_by_filename_only (Some id) f
   | None ->
diff --git a/library/nameops.ml b/library/nameops.ml
new file mode 100644
index 000000000..b7609bafd
--- /dev/null
+++ b/library/nameops.ml
@@ -0,0 +1,228 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Util
+open Names
+open Declarations
+open Environ
+open Term
+
+(* Identifiers *)
+
+let wildcard = id_of_string "_"
+
+(* Utilities *)
+
+let code_of_0 = Char.code '0'
+let code_of_9 = Char.code '9'
+
+let cut_ident s =
+  let s = string_of_id s in
+  let slen = String.length s in
+  (* [n'] is the position of the first non nullary digit *)
+  let rec numpart n n' =
+    if n = 0 then 
+      failwith
+	("The string " ^ s ^ " is not an identifier: it contains only digits")
+    else 
+      let c = Char.code (String.get s (n-1)) in
+      if c = code_of_0 && n <> slen then 
+	numpart (n-1) n' 
+      else if code_of_0 <= c && c <= code_of_9 then 
+	numpart (n-1) (n-1)
+      else 
+	n'
+  in
+  numpart slen slen
+
+let repr_ident s =
+  let numstart = cut_ident s in
+  let s = string_of_id s in
+  let slen = String.length s in
+  if numstart = slen then 
+    (s, None)
+  else
+    (String.sub s 0 numstart,
+     Some (int_of_string (String.sub s numstart (slen - numstart))))
+
+let make_ident sa = function
+  | Some n -> 
+      let c = Char.code (String.get sa (String.length sa -1)) in
+      let s =
+        if c < code_of_0 or c > code_of_9 then sa ^ (string_of_int n)
+        else sa ^ "_" ^ (string_of_int n) in
+      id_of_string s
+  | None -> id_of_string (String.copy sa)
+
+(* Rem: semantics is a bit different, if an ident starts with toto00 then
+  after successive renamings it comes to toto09, then it goes on with toto10 *)
+let lift_subscript id =
+  let id = string_of_id id in
+  let len = String.length id in
+  let rec add carrypos =
+    let c = id.[carrypos] in
+    if is_digit c then
+      if c = '9' then begin
+	assert (carrypos>0);
+	add (carrypos-1)
+      end
+      else begin
+	let newid = String.copy id in
+	String.fill newid (carrypos+1) (len-1-carrypos) '0';
+	newid.[carrypos] <- Char.chr (Char.code c + 1);
+	newid
+      end
+    else begin
+      let newid = id^"0" in
+      if carrypos < len-1 then begin
+	String.fill newid (carrypos+1) (len-1-carrypos) '0';
+	newid.[carrypos+1] <- '1'
+      end;
+      newid
+    end
+  in id_of_string (add (len-1))
+
+let has_subscript id =
+  let id = string_of_id id in
+  is_digit (id.[String.length id - 1])
+
+let forget_subscript id =
+  let numstart = cut_ident id in
+  let newid = String.make (numstart+1) '0' in
+  String.blit (string_of_id id) 0 newid 0 numstart;
+  (id_of_string newid)
+
+let add_suffix id s = id_of_string (string_of_id id ^ s)
+let add_prefix s id = id_of_string (s ^ string_of_id id)
+
+let atompart_of_id id = fst (repr_ident id)
+
+(* Fresh names *)
+
+let lift_ident = lift_subscript
+
+let next_ident_away id avoid = 
+  if List.mem id avoid then
+    let id0 = if not (has_subscript id) then id else 
+    (* Ce serait sans doute mieux avec quelque chose inspiré de 
+       *** make_ident id (Some 0) *** mais ça brise la compatibilité... *)
+    forget_subscript id in
+    let rec name_rec id =
+      if List.mem id avoid then name_rec (lift_ident id) else id in 
+    name_rec id0
+  else id
+
+let next_ident_away_from id avoid = 
+  let rec name_rec id =
+    if List.mem id avoid then name_rec (lift_ident id) else id in 
+  name_rec id 
+
+(* Names *)
+
+let out_name = function
+  | Name id -> id
+  | Anonymous -> anomaly "out_name: expects a defined name"
+
+let next_name_away_with_default default name l = 
+  match name with
+    | Name str  -> next_ident_away str l
+    | Anonymous -> next_ident_away (id_of_string default) l
+
+let next_name_away name l = 
+  match name with
+    | Name str  -> next_ident_away str l
+    | Anonymous -> id_of_string "_"
+
+(**********************************************)
+(* Operations on dirpaths *)
+let empty_dirpath = make_dirpath []
+
+let default_module_name = id_of_string "Top"
+let default_module = make_dirpath [default_module_name]
+
+(*s Roots of the space of absolute names *)
+let coq_root = id_of_string "Coq"
+let default_root_prefix = make_dirpath []
+
+let restrict_path n sp =
+  let dir, s = repr_path sp in
+  let (dir',_) = list_chop n (repr_dirpath dir) in
+  Names.make_path (make_dirpath dir') s
+
+(* Pop the last n module idents *)
+let extract_dirpath_prefix n dir =
+  let (_,dir') = list_chop n (repr_dirpath dir) in
+  make_dirpath dir'
+
+let dirpath_prefix p = match repr_dirpath p with
+  | [] -> anomaly "dirpath_prefix: empty dirpath"
+  | _::l -> make_dirpath l
+
+let is_dirpath_prefix_of d1 d2 =
+  list_prefix_of (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2))
+
+(* To know how qualified a name should be to be understood in the current env*)
+let add_dirpath_prefix id d = make_dirpath (repr_dirpath d @ [id])
+
+let split_dirpath d =
+  let l = repr_dirpath d in (make_dirpath (List.tl l), List.hd l)
+
+let extend_dirpath p id = make_dirpath (id :: repr_dirpath p)
+
+
+(* Section paths *)
+
+let dirpath sp = let (p,_) = repr_path sp in p
+let basename sp = let (_,id) = repr_path sp in id
+
+let path_of_constructor env ((sp,tyi),ind) =
+   let mib = Environ.lookup_mind sp env in
+   let mip = mib.mind_packets.(tyi) in 
+   let (pa,_) = repr_path sp in 
+   Names.make_path pa (mip.mind_consnames.(ind-1))
+
+let path_of_inductive env (sp,tyi) =
+  if tyi = 0 then sp
+  else
+    let mib = Environ.lookup_mind sp env in
+    let mip = mib.mind_packets.(tyi) in 
+    let (pa,_) = repr_path sp in 
+    Names.make_path pa (mip.mind_typename) 
+
+(* parsing *)
+let parse_sp s =
+  let len = String.length s in
+  let rec decoupe_dirs n =
+    try
+      let pos = String.index_from s n '.' in
+      let dir = String.sub s n (pos-n) in
+      let dirs,n' = decoupe_dirs (succ pos) in
+      (id_of_string dir)::dirs,n'
+    with
+      | Not_found -> [],n
+  in
+  if len = 0 then invalid_arg "parse_section_path";
+  let dirs,n = decoupe_dirs 0 in
+  let id = String.sub s n (len-n) in
+  make_dirpath (List.rev dirs), (id_of_string id)
+
+let dirpath_of_string s =
+  try
+    let sl,s = parse_sp s in
+    extend_dirpath sl s
+  with
+    | Invalid_argument _ -> invalid_arg "dirpath_of_string"
+
+let path_of_string s =
+  try
+    let sl,s = parse_sp s in
+    make_path sl s
+  with
+    | Invalid_argument _ -> invalid_arg "path_of_string"
diff --git a/library/nameops.mli b/library/nameops.mli
new file mode 100644
index 000000000..fc5bc6a6a
--- /dev/null
+++ b/library/nameops.mli
@@ -0,0 +1,71 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Names
+open Term
+open Environ
+
+(* Identifiers and names *)
+val wildcard : identifier
+
+val make_ident : string -> int option -> identifier
+val repr_ident : identifier -> string * int option
+
+val atompart_of_id : identifier -> string
+
+val add_suffix : identifier -> string -> identifier
+val add_prefix : string -> identifier -> identifier
+
+val lift_ident           : identifier -> identifier
+val next_ident_away      : identifier -> identifier list -> identifier
+val next_ident_away_from : identifier -> identifier list -> identifier
+
+val next_name_away : name -> identifier list -> identifier
+val next_name_away_with_default :
+  string -> name -> identifier list -> identifier
+
+val out_name : name -> identifier
+
+(* Section and module mechanism: dealinng with dir paths *)
+val empty_dirpath : dir_path
+val default_module : dir_path
+
+(* This is the root of the standard library of Coq *)
+val coq_root : module_ident
+
+(* This is the default root prefix for developments which doesn't
+   mention a root *)
+val default_root_prefix : dir_path
+
+
+val dirpath_of_string : string -> dir_path
+val path_of_string : string -> section_path
+
+val path_of_constructor : env -> constructor -> section_path
+val path_of_inductive   : env -> inductive -> section_path
+
+
+val dirpath : section_path -> dir_path
+val basename : section_path -> identifier
+
+(* Give the immediate prefix of a [dir_path] *)
+val dirpath_prefix : dir_path -> dir_path 
+
+(* Give the immediate prefix and basename of a [dir_path] *)
+val split_dirpath : dir_path -> dir_path * identifier
+
+val extend_dirpath : dir_path -> module_ident -> dir_path
+val add_dirpath_prefix : module_ident -> dir_path -> dir_path
+
+val extract_dirpath_prefix : int -> dir_path -> dir_path
+val is_dirpath_prefix_of : dir_path -> dir_path -> bool
+
+val restrict_path : int -> section_path -> section_path
+
diff --git a/library/nametab.ml b/library/nametab.ml
index 309841796..9348ff30d 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -11,21 +11,20 @@
 open Util
 open Pp
 open Names
+open Nameops
+open Declarations
 
 (*s qualified names *)
-type qualid = dir_path * identifier
+type qualid = section_path
 
-let make_qualid p id = (p,id)
-let repr_qualid q = q
+let make_qualid = make_path
+let repr_qualid = repr_path
 
-let empty_dirpath = make_dirpath []
-let make_short_qualid id = (empty_dirpath,id)
+let string_of_qualid = string_of_path
+let pr_qualid = pr_sp
 
-let string_of_qualid (l,id) = string_of_path (make_path l id CCI)
-
-let pr_qualid p = pr_str (string_of_qualid p)
-
-let qualid_of_sp sp = make_qualid (dirpath sp) (basename sp)
+let qualid_of_sp sp = sp
+let make_short_qualid id = make_qualid empty_dirpath id
 let qualid_of_dirpath dir = 
   let (l,a) = split_dirpath dir in
   make_qualid l a
@@ -41,24 +40,38 @@ let error_global_constant_not_found_loc loc q =
 
 let error_global_not_found q = raise (GlobalizationError q)
 
-(*s Roots of the space of absolute names *)
-
-let coq_root = id_of_string "Coq"
-let default_root_prefix = make_dirpath []
-
-(* Obsolète
-let roots = ref []
-let push_library_root = function
-  | [] -> ()
-  | s::_ -> roots := list_add_set s !roots
-*)
-let push_library_root s = ()
-
 (* Constructions and syntactic definitions live in the same space *)
+type global_reference =
+  | VarRef of variable
+  | ConstRef of constant
+  | IndRef of inductive
+  | ConstructRef of constructor
+
 type extended_global_reference =
   | TrueGlobal of global_reference
   | SyntacticDef of section_path
 
+let sp_of_global env = function
+  | VarRef id -> make_path empty_dirpath id
+  | ConstRef sp -> sp
+  | IndRef (sp,tyi) -> 
+      (* Does not work with extracted inductive types when the first 
+	 inductive is logic : if tyi=0 then basename sp else *)
+      let mib = Environ.lookup_mind sp env in
+      assert (tyi < mib.mind_ntypes && tyi >= 0);
+      let mip = mib.mind_packets.(tyi) in
+      let (p,_) = repr_path sp in
+      make_path p mip.mind_typename
+  | ConstructRef ((sp,tyi),i) ->
+      let mib = Environ.lookup_mind sp env in
+      assert (tyi < mib.mind_ntypes && i >= 0);
+      let mip = mib.mind_packets.(tyi) in
+      assert (i <= Array.length mip.mind_consnames && i > 0);
+      let (p,_) = repr_path sp in
+      make_path p mip.mind_consnames.(i-1)
+
+
+(* Dictionaries of short names *)
 type 'a nametree = ('a option * 'a nametree ModIdmap.t)
 type ccitab = extended_global_reference nametree Idmap.t
 type objtab = section_path nametree Idmap.t
@@ -69,15 +82,19 @@ let the_libtab = ref (ModIdmap.empty : dirtab)
 let the_sectab = ref (ModIdmap.empty : dirtab)
 let the_objtab = ref (Idmap.empty : objtab)
 
-let dirpath_of_reference = function
-  | ConstRef sp -> dirpath sp
-  | VarRef sp -> dirpath sp
-  | ConstructRef ((sp,_),_) -> dirpath sp
-  | IndRef (sp,_) -> dirpath sp
+let dirpath_of_reference ref =
+  let sp = match ref with
+    | ConstRef sp -> sp
+    | VarRef id -> make_path empty_dirpath id
+    | ConstructRef ((sp,_),_) -> sp
+    | IndRef (sp,_) -> sp in
+  let (p,_) = repr_path sp in
+  p
 
 let dirpath_of_extended_ref = function
   | TrueGlobal ref -> dirpath_of_reference ref
-  | SyntacticDef sp -> dirpath sp
+  | SyntacticDef sp ->
+      let (p,_) = repr_path sp in p
 
 (* How [visibility] works: a value of [0] means all suffixes of [dir] are
    allowed to access the object, a value of [1] means all suffixes, except the
@@ -94,7 +111,7 @@ let dirpath_of_extended_ref = function
 (* We add a binding of [[modid1;...;modidn;id]] to [o] in the name tab *)
 (* We proceed in the reverse way, looking first to [id] *)
 let push_tree extract_dirpath tab visibility dir o =
-  let extract = option_app (fun c -> rev_repr_dirpath (extract_dirpath c)) in
+  let extract = option_app (fun c -> repr_dirpath (extract_dirpath c)) in
   let rec push level (current,dirmap) = function
     | modid :: path as dir ->
 	let mc = 
@@ -112,7 +129,7 @@ let push_tree extract_dirpath tab visibility dir o =
           else current in
 	(this, ModIdmap.add modid (push (level+1) mc path) dirmap)
     | [] -> (Some o,dirmap) in
-  push 0 tab (rev_repr_dirpath dir)
+  push 0 tab (repr_dirpath dir)
 
 let push_idtree extract_dirpath tab n dir id o =
   let modtab =
@@ -122,7 +139,8 @@ let push_idtree extract_dirpath tab n dir id o =
 
 let push_long_names_ccipath = push_idtree dirpath_of_extended_ref the_ccitab
 let push_short_name_ccipath = push_idtree dirpath_of_extended_ref the_ccitab
-let push_short_name_objpath = push_idtree dirpath the_objtab
+let push_short_name_objpath =
+  push_idtree (fun sp -> let (p,_) = repr_path sp in p) the_objtab
 
 let push_modidtree tab dir id o =
   let modtab =
@@ -140,7 +158,7 @@ let push_long_names_libpath = push_modidtree the_libtab
    Parameter but also Remark and Fact) *)
 
 let push_cci n sp ref =
-  let dir, s = repr_qualid (qualid_of_sp sp) in
+  let dir, s = repr_path sp in
   (* We push partially qualified name (with at least one prefix) *)
   push_long_names_ccipath n dir s (TrueGlobal ref)
 
@@ -149,7 +167,7 @@ let push = push_cci
 (* This is for Syntactic Definitions *)
 
 let push_syntactic_definition sp =
-  let dir, s = repr_qualid (qualid_of_sp sp) in
+  let dir, s = repr_path sp in
   push_long_names_ccipath 0 dir s (SyntacticDef sp)
 
 let push_short_name_syntactic_definition sp =
@@ -164,7 +182,6 @@ let push_short_name_object sp =
   push_short_name_objpath 0 empty_dirpath s sp
 
 (* This is to remember absolute Section/Module names and to avoid redundancy *)
-
 let push_section fulldir =
   let dir, s = split_dirpath fulldir in
   (* We push all partially qualified name *)
@@ -173,7 +190,7 @@ let push_section fulldir =
 
 (* These are entry points to locate names *)
 let locate_in_tree tab dir =
-  let dir = rev_repr_dirpath dir in
+  let dir = repr_dirpath dir in
   let rec search (current,modidtab) = function
     | modid :: path -> search (ModIdmap.find modid modidtab) path
     | [] -> match current with Some o -> o | _ -> raise Not_found
@@ -217,10 +234,9 @@ let locate_constant qid =
   (* TODO: restrict to defined constants *)
   match locate_cci qid with
     | TrueGlobal (ConstRef sp) -> sp
-    | TrueGlobal (VarRef sp) -> sp
     | _ -> raise Not_found
 
-let sp_of_id _ id = match locate_cci (make_short_qualid id) with
+let sp_of_id id = match locate_cci (make_short_qualid id) with
   | TrueGlobal ref -> ref
   | SyntacticDef _ ->
       anomaly ("sp_of_id: "^(string_of_id id)
@@ -232,15 +248,16 @@ let constant_sp_of_id id =
     | _ -> raise Not_found
 
 let absolute_reference sp =
-  let a = locate_cci (qualid_of_sp sp) in
-  if not (dirpath_of_extended_ref a = dirpath sp) then
+  let a = locate_cci sp in
+  let (p,_) = repr_path sp in
+  if not (dirpath_of_extended_ref a = p) then
     anomaly ("Not an absolute path: "^(string_of_path sp));
   match a with
     | TrueGlobal ref -> ref
     | _ -> raise Not_found
 
 let locate_in_absolute_module dir id =
-  absolute_reference (make_path dir id CCI)
+  absolute_reference (make_path dir id)
 
 let global loc qid =
   try match extended_locate qid with
@@ -253,13 +270,28 @@ let global loc qid =
     error_global_not_found_loc loc qid
 
 let exists_cci sp =
-  try let _ = locate_cci (qualid_of_sp sp) in true
+  try let _ = locate_cci sp in true
   with Not_found -> false
 
 let exists_section dir =
   try let _ = locate_section (qualid_of_dirpath dir) in true
   with Not_found -> false
 
+
+(* For a sp Coq.A.B.x, try to find the shortest among x, B.x, A.B.x
+   and Coq.A.B.x is a qualid that denotes the same object. *)
+let qualid_of_global env ref =  
+  let sp = sp_of_global env ref in
+  let (pth,id) = repr_path sp in
+  let rec find_visible dir qdir =
+    let qid = make_qualid qdir id in
+    if (try locate qid = ref with Not_found -> false) then qid
+    else match dir with
+      | [] -> qualid_of_sp sp
+      | a::l -> find_visible l (add_dirpath_prefix a qdir)
+  in
+  find_visible (repr_dirpath pth) (make_dirpath [])
+
 (********************************************************************)
 
 (********************************************************************)
@@ -272,21 +304,18 @@ let init () =
   the_libtab := ModIdmap.empty;
   the_sectab := ModIdmap.empty;
   the_objtab := Idmap.empty
-(*  ;roots := []*)
 
 let freeze () =
   !the_ccitab, 
   !the_libtab,
   !the_sectab,
   !the_objtab
-(*  ,!roots*)
 
-let unfreeze (mc,ml,ms,mo(*,r*)) =
+let unfreeze (mc,ml,ms,mo) =
   the_ccitab := mc;
   the_libtab := ml;
   the_sectab := ms;
-  the_objtab := mo(*;
-  roots := r*)
+  the_objtab := mo
 
 let _ = 
   Summary.declare_summary "names"
diff --git a/library/nametab.mli b/library/nametab.mli
index 5fb7eb237..6cf3f8673 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -17,6 +17,16 @@ open Names
 (*s This module contains the table for globalization, which associates global
    names (section paths) to qualified names. *)
 
+type global_reference =
+  | VarRef of variable
+  | ConstRef of constant
+  | IndRef of inductive
+  | ConstructRef of constructor
+
+(* Finds the real name of a global (e.g. fetch the constructor names
+   from the inductive name and constructor number) *)
+val sp_of_global : Environ.env -> global_reference -> section_path
+
 type extended_global_reference =
   | TrueGlobal of global_reference
   | SyntacticDef of section_path
@@ -33,9 +43,11 @@ val make_short_qualid : identifier -> qualid
 val string_of_qualid : qualid -> string
 val pr_qualid : qualid -> std_ppcmds
 
-(* Turns an absolute name into a qualified name denoting the same name *)
 val qualid_of_sp : section_path -> qualid
 
+(* Turns an absolute name into a qualified name denoting the same name *)
+val qualid_of_global : Environ.env -> global_reference -> qualid
+
 exception GlobalizationError of qualid
 exception GlobalizationConstantError of qualid
 
@@ -56,7 +68,7 @@ val push_short_name_object : section_path -> unit
 val push_section : dir_path -> unit
 
 (* This should eventually disappear *)
-val sp_of_id : path_kind -> identifier -> global_reference
+val sp_of_id : identifier -> global_reference
 
 (*s The following functions perform globalization of qualified names *)
 
@@ -83,15 +95,6 @@ val exists_section : dir_path -> bool
 
 (*s Roots of the space of absolute names *)
 
-(* This is the root of the standard library of Coq *)
-val coq_root : module_ident
-
-(* This is the default root prefix for developments which doesn't mention a root *)
-val default_root_prefix : dir_path
-
-(* This is to declare a new root *)
-val push_library_root : dir_path -> unit
-
 (* This turns a "user" absolute name into a global reference;
    especially, constructor/inductive names are turned into internal
    references inside a block of mutual inductive *)
diff --git a/library/opaque.ml b/library/opaque.ml
index 26d2798b1..c672454a5 100644
--- a/library/opaque.ml
+++ b/library/opaque.ml
@@ -38,7 +38,8 @@ let is_evaluable env ref =
     | EvalVarRef id ->
         let (ids,sps) = !tr_state in
         Idpred.mem id ids &
-        Environ.lookup_named_value id env <> None
+        let (_,value,_) = Environ.lookup_named id env in
+        value <> None
 
 (* Modifying this state *)
 let set_opaque_const sp =
@@ -48,8 +49,8 @@ let set_transparent_const sp =
   let (ids,sps) = !tr_state in
   let cb = Global.lookup_constant sp in
   if cb.const_body <> None & cb.const_opaque then
-    error ("Cannot make "^Global.string_of_global (ConstRef sp)^
-           " transparent because it was declared opaque.");
+    let s = string_of_path sp in
+    error ("Cannot make "^s^" transparent because it was declared opaque.");
   tr_state := (ids, Sppred.add sp sps)
 
 let set_opaque_var id =