Parsing

- Typage renforcé dans les grammaires (distinction des vars et des metavars)
- Disparition de SLAM au profit de ABSTRACT
- Paths primitifs dans les quotations (syntaxe concrète à base de .)
- Mise en place de identifier dès le type ast
- Protection de identifier contre les effets de bord via un String.copy
- Utilisation de module_ident (= identifier) dans les dir_path (au
  lieu de string)

Table des noms qualifiés

- Remplacement de la table de visibilité par une table qui ne cache
  plus les noms de modules et sections mais seulement les noms des
  constantes (e.g. Require A. ne cachera plus le contenu d'un éventuel
  module A déjà existant : seuls les noms de constructions de l'ancien
  A qui existent aussi dans le nouveau A seront cachés)
- Renoncement à la possibilité d'accéder les formes non déchargées des
  constantes définies à l'intérieur de sections et simplification
  connexes (suppression de END-SECTION, une seule table de noms qui ne
  survit pas au discharge)
- Utilisation de noms longs pour les modules, de noms qualifiés pour
  Require and co, tests de cohérence; pour être cohérent avec la non
  survie des tables de noms à la sortie des section, les require à
  l'intérieur d'une section eux aussi sont refaits à la fermeture de la
  section


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

8 files changed, 157 insertions, 216 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 7a06a7896..482be2fb9 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -25,7 +25,7 @@ type modification_action = ABSTRACT | ERASE
 type 'a modification =
   | NOT_OCCUR
   | DO_ABSTRACT of 'a * modification_action list
-  | DO_REPLACE
+  | DO_REPLACE of constant_body
 
 type work_list =
     (section_path * section_path modification) list
@@ -33,7 +33,7 @@ type work_list =
     * (constructor_path * constructor_path modification) list
 
 type recipe = {
-  d_from : section_path;
+  d_from : constant_body;
   d_abstract : identifier list;
   d_modlist : work_list }
 
@@ -83,7 +83,7 @@ let modify_opers replfun absfun (constl,indl,cstrl) =
 		| DO_ABSTRACT (oper',modif) ->
 		    assert (List.length modif <= Array.length cl);
 		    interp_modif absfun mkMutInd (oper',modif) cl'
-		| DO_REPLACE -> assert false)
+		| DO_REPLACE _ -> assert false)
 	   with 
 	     | Not_found -> mkMutInd (spi,cl'))
 
@@ -94,7 +94,7 @@ let modify_opers replfun absfun (constl,indl,cstrl) =
 		| DO_ABSTRACT (oper',modif) ->
 		    assert (List.length modif <= Array.length cl);
 		    interp_modif absfun mkMutConstruct (oper',modif) cl'
-		| DO_REPLACE -> assert false)
+		| DO_REPLACE _ -> assert false)
 	   with 
 	     | Not_found -> mkMutConstruct (spi,cl'))
 
@@ -105,7 +105,7 @@ let modify_opers replfun absfun (constl,indl,cstrl) =
 		| DO_ABSTRACT (oper',modif) ->
 		    assert (List.length modif <= Array.length cl);
 		    interp_modif absfun mkConst (oper',modif) cl'
-		| DO_REPLACE -> substrec (replfun (sp,cl')))
+		| DO_REPLACE cb -> substrec (replfun sp cb cl'))
 	   with 
 	     | Not_found -> mkConst (sp,cl'))
   
@@ -117,17 +117,18 @@ let expmod_constr oldenv modlist c =
   let sigma = Evd.empty in
   let simpfun = 
     if modlist = ([],[],[]) then fun x -> x else nf_betaiota in
-  let expfun cst = 
-    try 
-      constant_value oldenv cst
-    with NotEvaluableConst Opaque ->
-      let (sp,_) = cst in
+  let expfun sp cb args = 
+    if cb.const_opaque then
       errorlabstrm "expmod_constr"
 	[< 'sTR"Cannot unfold the value of ";
-           'sTR(string_of_path sp); 'sPC;
-           'sTR"You cannot declare local lemmas as being opaque"; 'sPC;
-           'sTR"and then require that theorems which use them"; 'sPC;
-           'sTR"be transparent" >];
+        'sTR(string_of_path sp); 'sPC;
+        'sTR"You cannot declare local lemmas as being opaque"; 'sPC;
+        'sTR"and then require that theorems which use them"; 'sPC;
+        'sTR"be transparent" >];
+    match cb.const_body with
+      | Some body -> 
+          instantiate_constr cb.const_hyps body (Array.to_list args)
+      | None -> assert false
   in
   let c' = modify_opers expfun (fun a b -> mkApp (a, [|b|])) modlist c in
   match kind_of_term c' with
@@ -155,7 +156,7 @@ let abstract_constant ids_to_abs hyps (body,typ) =
   (body',typ')
 
 let cook_constant env r =
-  let cb = lookup_constant r.d_from env in
+  let cb = r.d_from in
   let typ = expmod_type env r.d_modlist cb.const_type in
   let body = option_app (expmod_constr env r.d_modlist) cb.const_body in
   let hyps = List.map (fun (sp,c,t) -> (basename sp,c,t)) cb.const_hyps in
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index f29503176..d9b564835 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -20,7 +20,7 @@ type modification_action = ABSTRACT | ERASE
 type 'a modification =
   | NOT_OCCUR
   | DO_ABSTRACT of 'a * modification_action list
-  | DO_REPLACE
+  | DO_REPLACE of constant_body
 
 type work_list =
     (section_path * section_path modification) list
@@ -28,7 +28,7 @@ type work_list =
     * (constructor_path * constructor_path modification) list
 
 type recipe = {
-  d_from : section_path;
+  d_from : constant_body;
   d_abstract : identifier list;
   d_modlist : work_list }
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index db187880f..77b96d30c 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -20,7 +20,7 @@ open Declarations
 
 type checksum = int
 
-type import = string * checksum
+type compilation_unit_name = dir_path * checksum
 
 type global = Constant | Inductive
 
@@ -28,7 +28,7 @@ type globals = {
   env_constants : constant_body Spmap.t;
   env_inductives : mutual_inductive_body Spmap.t;
   env_locals : (global * section_path) list;
-  env_imports : import list }
+  env_imports : compilation_unit_name list }
 
 type context = {
   env_named_context : named_context;
@@ -366,9 +366,8 @@ let set_transparent env sp =
 (*s Modules (i.e. compiled environments). *)
 
 type compiled_env = {
-  cenv_id : string;
-  cenv_stamp : checksum;
-  cenv_needed : import list;
+  cenv_stamped_id : compilation_unit_name;
+  cenv_needed : compilation_unit_name list;
   cenv_constants : (section_path * constant_body) list;
   cenv_inductives : (section_path * mutual_inductive_body) list }
 
@@ -382,8 +381,7 @@ let exported_objects env =
 
 let export env id = 
   let (cst,ind) = exported_objects env in
-  { cenv_id = id;
-    cenv_stamp = 0;
+  { cenv_stamped_id = (id,0);
     cenv_needed = env.env_globals.env_imports;
     cenv_constants = cst;
     cenv_inductives = ind }
@@ -394,9 +392,9 @@ let check_imports env needed =
     try
       let actual_stamp = List.assoc id imports in
       if stamp <> actual_stamp then
-	error ("Inconsistent assumptions over module " ^ id)
+	error ("Inconsistent assumptions over module " ^(string_of_dirpath id))
     with Not_found -> 
-      error ("Reference to unknown module " ^ id)
+      error ("Reference to unknown module " ^ (string_of_dirpath id))
   in
   List.iter check needed
 
@@ -415,7 +413,7 @@ let import cenv env =
     { env_constants = add_list gl.env_constants cenv.cenv_constants;
       env_inductives = add_list gl.env_inductives cenv.cenv_inductives;
       env_locals = gl.env_locals;
-      env_imports = (cenv.cenv_id,cenv.cenv_stamp) :: gl.env_imports }
+      env_imports = cenv.cenv_stamped_id :: gl.env_imports }
   in
   let g = universes env in
   let g = List.fold_left 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index ca93b84e7..45c2d1130 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -173,7 +173,7 @@ val set_transparent : env -> constant_path -> unit
 
 type compiled_env
 
-val export : env -> string -> compiled_env
+val export : env -> dir_path -> compiled_env
 val import : compiled_env -> env -> env
 
 (*s Unsafe judgments. We introduce here the pre-type of judgments, which is
diff --git a/kernel/names.ml b/kernel/names.ml
index 4965a733c..c4ced8e99 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -11,101 +11,16 @@
 open Pp
 open Util
 
+(*s Identifiers *)
+
 (* Utilities *)
 
 let code_of_0 = Char.code '0'
 let code_of_9 = Char.code '9'
 
-(* This checks that a string is acceptable as an ident, i.e. starts
-   with a letter and contains only letters, digits or "'" *)
-
-let check_ident_suffix i l s =
-  for i=1 to l-1 do
-    let c = String.get s i in
-    if not (is_letter c or is_digit c or c = '\'') then
-      error
-	("Character "^(String.sub s i 1)^" is not allowed in an identifier")
-  done
-
-let check_ident s =
-  let l = String.length s in
-  if l = 0 then error "The empty string is not an identifier"; 
-  let c = String.get s 0 in
-  if not (is_letter c) then error "An identifier starts with a letter";
-  check_ident_suffix 1 l s
-
-let check_suffix s = check_ident_suffix 0 (String.length s) s
-
-let is_ident s = try check_ident s; true with _ -> false
-
 (* Identifiers *)
-(*
-module Ident = struct
-
-type t = {
-  atom : string ; 
-  index : int }
-
-let repr_ident { atom = sa; index = n } =
-  if n = -1 then (sa,None) else (sa,Some n)
-
-let make_ident sa = function
-  | Some n ->
-      let c = Char.code (String.get sa (String.length sa -1)) in
-      if c < code_of_0 or c > code_of_9 then { atom = sa; index = n }
-      else { atom = sa^"_"; index = n }
-  | None -> { atom = sa; index = -1 }
-
-let string_of_id id = match repr_ident id with
-  | (s,None) -> s
-  | (s,Some n) -> s ^ (string_of_int n)
-
-let id_of_string s =
-  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
-  let numstart = numpart slen slen in
-  if numstart = slen then 
-    { atom = s; index = -1 } 
-  else
-    { atom = String.sub s 0 numstart;
-      index = int_of_string (String.sub s numstart (slen - numstart)) }
-
-let first_char id =
-  assert (id.atom <> "");
-  String.make 1 id.atom.[0]
-
-let id_ord { atom = s1; index = n1 } { atom = s2; index = n2 } = 
-  let s_bit = Pervasives.compare s1 s2 in
-  if s_bit = 0 then n1 - n2 else s_bit
 
-(* Rem : if an ident starts with toto00 then after successive
-   renamings it comes to toto09, then it goes on with toto010 *)
-let lift_ident { atom = str; index = i } = { atom = str; index = i+1 }
-let restart_ident id = { id with index = 0 }
-let has_index id = (id.index <> -1)
-
-let hash_sub hstr id = { atom = hstr id.atom; index = id.index }
-let equal id1 id2 = id1.atom == id2.atom && id1.index = id2.index
-
-end (* End of module Ident *)
-*)
-(* Second implementation *)
-module Ident = struct
-
-type t = string
+type identifier = string
 
 let cut_ident s =
   let slen = String.length s in
@@ -139,13 +54,7 @@ let make_ident sa = function
       let c = Char.code (String.get sa (String.length sa -1)) in
       if c < code_of_0 or c > code_of_9 then sa ^ (string_of_int n)
       else sa ^ "_" ^ (string_of_int n)
-  | None -> sa
-
-let add_suffix id s = check_suffix s; id^s
-let add_prefix s id = check_ident s; s^id
-
-let string_of_id id = id
-let id_of_string s = s
+  | None -> String.copy sa
 
 let first_char id =
   assert (id <> "");
@@ -155,7 +64,7 @@ let id_ord = Pervasives.compare
 
 (* 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_ident id =
+let lift_subscript id =
   let len = String.length id in
   let rec add carrypos =
     let c = id.[carrypos] in
@@ -180,28 +89,52 @@ let lift_ident id =
     end
   in add (len-1)
 
-let has_index id = is_digit (id.[String.length id - 1])
+let has_subscript id = is_digit (id.[String.length id - 1])
 
-let restart_ident id =
+let forget_subscript id =
   let len = String.length id in
   let numstart = cut_ident id in
   let newid = String.make (numstart+1) '0' in
   String.blit id 0 newid 0 numstart;
   newid
 
-let hash_sub hstr id = hstr id
-let equal id1 id2 = id1 == id2
+(* This checks that a string is acceptable as an ident, i.e. starts
+   with a letter and contains only letters, digits or "'" *)
+
+let check_ident_suffix i l s =
+  for i=1 to l-1 do
+    let c = String.get s i in
+    if not (is_letter c or is_digit c or c = '\'' or c = '_' or c = '@') then
+      error
+	("Character "^(String.sub s i 1)^" is not allowed in an identifier")
+  done
+
+let check_ident s =
+  let l = String.length s in
+  if l = 0 then error "The empty string is not an identifier";
+  let c = String.get s 0 in
+  if (is_letter c) or c = '_' or c = '$' then check_ident_suffix 1 l s
+  else error (s^": an identifier starts with a letter")
+
+let is_ident s = try check_ident s; true with _ -> false
 
-end (* End of module Ident *)
+let check_suffix s = check_ident_suffix 0 (String.length s) s
 
-type identifier = Ident.t
-let repr_ident = Ident.repr_ident
-let make_ident = Ident.make_ident
 let add_suffix id s = check_suffix s; id^s
 let add_prefix s id = check_ident s; s^id
-let string_of_id = Ident.string_of_id
-let id_of_string = Ident.id_of_string
-let id_ord = Ident.id_ord
+
+let string_of_id id = String.copy id
+let id_of_string s = check_ident s; String.copy s
+
+(* Hash-consing of identifier *)
+module Hident = Hashcons.Make(
+  struct 
+    type t = string
+    type u = string -> string
+    let hash_sub hstr id = hstr id
+    let equal id1 id2 = id1 == id2
+    let hash = Hashtbl.hash
+  end)
 
 module IdOrdered = 
   struct
@@ -216,18 +149,18 @@ let atompart_of_id id = fst (repr_ident id)
 let index_of_id id = snd (repr_ident id)
 let pr_id id = [< 'sTR (string_of_id id) >]
 
-let first_char = Ident.first_char
+let wildcard = id_of_string "_"
 
 (* Fresh names *)
 
-let lift_ident = Ident.lift_ident
+let lift_ident = lift_subscript
 
 let next_ident_away id avoid = 
   if List.mem id avoid then
-    let id0 = if not (Ident.has_index id) then id else 
+    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é... *)
-    Ident.restart_ident id in
+    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
@@ -272,30 +205,25 @@ let kind_of_string = function
   | _ -> invalid_arg "kind_of_string"
 
 (*s Directory paths = section names paths *)
-type dir_path = string list
-
-(*s Section paths are absolute names *)
+type module_ident = identifier
+type dir_path = module_ident list
 
-type section_path = {
-  dirpath : dir_path ;
-  basename : identifier ;
-  kind : path_kind }
+module ModIdOrdered = 
+  struct
+    type t = identifier
+    let compare = Pervasives.compare
+  end
 
-let make_path pa id k = { dirpath = pa; basename = id; kind = k }
-let repr_path { dirpath = pa; basename = id; kind = k} = (pa,id,k)
+module ModIdmap = Map.Make(ModIdOrdered)
 
-let kind_of_path sp = sp.kind
-let basename sp = sp.basename
-let dirpath sp = sp.dirpath
+let make_dirpath x = x
+let repr_dirpath x = x
 
-(* parsing and printing of section paths *)
-let string_of_dirpath sl = String.concat "." sl
+let dirpath_prefix = function 
+  | [] -> anomaly "dirpath_prefix: empty dirpath"
+  | l -> snd (list_sep_last l)
 
-let string_of_path sp =
-  let (sl,id,k) = repr_path sp in
-  String.concat ""
-    (List.flatten (List.map (fun s -> [s;"."]) sl)
-     @ [ string_of_id id ])
+let split_dirpath d = let (b,d) = list_sep_last d in (d,b)
 
 let parse_sp s =
   let len = String.length s in
@@ -304,37 +232,60 @@ let parse_sp s =
       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
-      dir::dirs,n'
+      (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
-  dirs,id
+  dirs, (id_of_string id)
 
-let path_of_string s =
+let dirpath_of_string s =
   try
     let sl,s = parse_sp s in
-    make_path sl (id_of_string s) CCI
+    sl @ [s]
   with
-    | Invalid_argument _ -> invalid_arg "path_of_string"
+    | Invalid_argument _ -> invalid_arg "dirpath_of_string"
 
-let dirpath_of_string s =
+let string_of_dirpath sl = String.concat "." (List.map string_of_id sl)
+
+let pr_dirpath sl = [< 'sTR (string_of_dirpath sl) >]
+
+(*s Section paths are absolute names *)
+
+type section_path = {
+  dirpath : dir_path ;
+  basename : identifier ;
+  kind : path_kind }
+
+let make_path pa id k = { dirpath = pa; basename = id; kind = k }
+let repr_path { dirpath = pa; basename = id; kind = k} = (pa,id,k)
+
+let kind_of_path sp = sp.kind
+let basename sp = sp.basename
+let dirpath sp = sp.dirpath
+
+(* parsing and printing of section paths *)
+let string_of_path sp =
+  let (sl,id,k) = repr_path sp in
+  (string_of_dirpath sl) ^ "." ^ (string_of_id id)
+
+let path_of_string s =
   try
     let sl,s = parse_sp s in
-    sl @ [s]
+    make_path sl s CCI
   with
-    | Invalid_argument _ -> invalid_arg "dirpath_of_string"
+    | Invalid_argument _ -> invalid_arg "path_of_string"
 
 let pr_sp sp = [< 'sTR (string_of_path sp) >]
 
 let sp_of_wd = function
   | [] -> invalid_arg "Names.sp_of_wd"
-  | l -> let (bn,dp) = list_sep_last l in make_path dp (id_of_string bn) OBJ
+  | l -> let (bn,dp) = list_sep_last l in make_path dp bn OBJ
 
 let wd_of_sp sp = 
-  let (sp,id,_) = repr_path sp in sp @ [string_of_id id]
+  let (sp,id,_) = repr_path sp in sp @ [id]
 
 let sp_ord sp1 sp2 =
   let (p1,id1,k) = repr_path sp1
@@ -346,7 +297,7 @@ let sp_ord sp1 sp2 =
   else
     ck
 
-let dirpath_prefix_of = list_prefix_of
+let is_dirpath_prefix_of = list_prefix_of
 
 module SpOrdered =
   struct
@@ -366,16 +317,6 @@ type inductive_path = section_path * int
 type constructor_path = inductive_path * int
 type mutual_inductive_path = section_path
 
-(* Hash-consing of identifier *)
-module Hident = Hashcons.Make(
-  struct 
-    type t = Ident.t
-    type u = string -> string
-    let hash_sub = Ident.hash_sub
-    let equal = Ident.equal
-    let hash = Hashtbl.hash
-  end)
-
 (* Hash-consing of name objects *)
 module Hname = Hashcons.Make(
   struct 
@@ -395,9 +336,9 @@ module Hname = Hashcons.Make(
 module Hsp = Hashcons.Make(
   struct 
     type t = section_path
-    type u = (identifier -> identifier) * (string -> string)
-    let hash_sub (hident,hstr) sp =
-      { dirpath = List.map hstr sp.dirpath;
+    type u = identifier -> identifier
+    let hash_sub hident sp =
+      { dirpath = List.map hident sp.dirpath;
         basename = hident sp.basename;
         kind = sp.kind }
     let equal sp1 sp2 =
@@ -411,6 +352,6 @@ let hcons_names () =
   let hstring = Hashcons.simple_hcons Hashcons.Hstring.f () in
   let hident = Hashcons.simple_hcons Hident.f hstring in
   let hname = Hashcons.simple_hcons Hname.f hident in
-  let hspcci = Hashcons.simple_hcons Hsp.f (hident,hstring) in
-  let hspfw = Hashcons.simple_hcons Hsp.f (hident,hstring) in
+  let hspcci = Hashcons.simple_hcons Hsp.f hident in
+  let hspfw = Hashcons.simple_hcons Hsp.f hident in
   (hspcci,hspfw,hname,hident,hstring)
diff --git a/kernel/names.mli b/kernel/names.mli
index 7eb39ff67..58aae5a65 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -32,10 +32,8 @@ val string_of_id : identifier -> string
 val id_of_string : string -> identifier
 val pr_id : identifier -> std_ppcmds
 
-(* These checks the validity of an identifier; [check_ident] fails
-   with error if invalid *)
-val check_ident : string -> unit
-val is_ident : string -> bool
+(* This is the identifier ["_"] *)
+val wildcard : identifier
 
 (* Deriving ident from other idents *)
 val add_suffix : identifier -> string -> identifier
@@ -63,10 +61,24 @@ val string_of_kind : path_kind -> string
 val kind_of_string : string -> path_kind
 
 (*s Directory paths = section names paths *)
-type dir_path = string list
+type module_ident = identifier
+type dir_path = module_ident list
+
+module ModIdmap : Map.S with type key = module_ident
+
+val make_dirpath : module_ident list -> dir_path
+val repr_dirpath : dir_path -> module_ident list
+
+(* 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
 
 (* Printing of directory paths as ["coq_root.module.submodule"] *)
 val string_of_dirpath : dir_path -> string
+val pr_dirpath : dir_path -> std_ppcmds
+
 
 (*s Section paths are {\em absolute} names *)
 type section_path
@@ -80,8 +92,8 @@ val dirpath : section_path -> dir_path
 val basename : section_path -> identifier
 val kind_of_path : section_path -> path_kind
 
-val sp_of_wd : string list -> section_path
-val wd_of_sp : section_path -> string list
+val sp_of_wd : module_ident list -> section_path
+val wd_of_sp : section_path -> module_ident list
 
 (* Parsing and printing of section path as ["coq_root.module.id"] *)
 val path_of_string : string -> section_path
@@ -89,25 +101,11 @@ val string_of_path : section_path -> string
 val pr_sp : section_path -> std_ppcmds
 val dirpath_of_string : string -> dir_path
 
-(*i
-val string_of_path_mind : section_path -> identifier -> string
-val coerce_path : path_kind -> section_path -> section_path
-val fwsp_of : section_path -> section_path
-val ccisp_of : section_path -> section_path
-val objsp_of : section_path -> section_path
-val fwsp_of_ccisp : section_path -> section_path
-val ccisp_of_fwsp : section_path -> section_path
-val append_to_path : section_path -> string -> section_path
-
-val sp_gt : section_path * section_path -> bool
-i*)
 val sp_ord : section_path -> section_path -> int
 
 (* [is_dirpath_prefix p1 p2=true] if [p1] is a prefix of or is equal to [p2] *)
-val dirpath_prefix_of : dir_path -> dir_path -> bool
-(*i
-module Spset : Set.S with type elt = section_path
-i*)
+val is_dirpath_prefix_of : dir_path -> dir_path -> bool
+
 module Spmap : Map.S with type key = section_path
 
 (*s Specific paths for declarations *)
@@ -121,4 +119,3 @@ type mutual_inductive_path = section_path
 val hcons_names : unit ->
   (section_path -> section_path) * (section_path -> section_path) *
   (name -> name) * (identifier -> identifier) * (string -> string)
-
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 04fbe21bb..102fbb228 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -63,7 +63,7 @@ val lookup_mind_specif : inductive -> safe_environment -> inductive_instance
 val set_opaque : safe_environment -> section_path -> unit
 val set_transparent : safe_environment -> section_path -> unit
 
-val export : safe_environment -> string -> compiled_env
+val export : safe_environment -> dir_path -> compiled_env
 val import : compiled_env -> safe_environment -> safe_environment
 
 val env_of_safe_env : safe_environment -> env
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 7c3060820..5f03e6a36 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -40,9 +40,12 @@ let string_of_univ u =
 let pr_uni u =
   [< 'sTR (Names.string_of_dirpath u.u_mod) ; 'sTR"." ; 'iNT u.u_num >]
 
-
-let dummy_univ = { u_mod = ["dummy univ"]; u_num = 0 } (* for prover terms *)
-let implicit_univ = { u_mod = ["implicit univ"]; u_num = 0 }
+let dummy_univ =  (* for prover terms *)
+  { u_mod = Names.make_dirpath [Names.id_of_string "dummy_univ"];
+    u_num = 0 }
+let implicit_univ =
+  { u_mod = Names.make_dirpath [Names.id_of_string "implicit_univ"];
+    u_num = 0 }
 
 let current_module = ref []
 
@@ -83,7 +86,7 @@ let declare_univ u g =
 (* The universes of Prop and Set: Type_0, Type_1 and the
    resulting graph. *)
 let (initial_universes,prop_univ,prop_univ_univ) =
-  let prop_sp = ["prop_univ"] in
+  let prop_sp = Names.make_dirpath [Names.id_of_string "prop_univ"] in
   let u = { u_mod = prop_sp; u_num = 0 } in
   let su = { u_mod = prop_sp; u_num = 1 } in
   let g = enter_arc (terminal u) UniverseMap.empty in
@@ -430,7 +433,7 @@ module Huniv =
   Hashcons.Make(
     struct
       type t = universe
-      type u = string -> string
+      type u = Names.identifier -> Names.identifier
       let hash_sub hstr {u_mod=sp; u_num=n} = 
 	{u_mod=List.map hstr sp; u_num=n}
       let equal {u_mod=sp1; u_num=n1} {u_mod=sp2; u_num=n2} =
@@ -441,5 +444,6 @@ module Huniv =
 
 
 let hcons1_univ u =
-  let hstring = Hashcons.simple_hcons Hashcons.Hstring.f () in
-  Hashcons.simple_hcons Huniv.f hstring u
+  let _,_,_,hid,_ = Names.hcons_names () in
+  Hashcons.simple_hcons Huniv.f hid u
+