Le bon choix, c'est finalement identifier = string

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

1 files changed, 3 insertions, 3 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index 6ae023888..08b1b58a0 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -37,7 +37,7 @@ let check_ident s =
 let is_ident s = try check_ident s; true with _ -> false
 
 (* Identifiers *)
-
+(*
 module Ident = struct
 
 type t = {
@@ -99,7 +99,7 @@ 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
 
@@ -188,7 +188,7 @@ let hash_sub hstr id = hstr id
 let equal id1 id2 = id1 == id2
 
 end (* End of module Ident *)
-*)
+
 type identifier = Ident.t
 let repr_ident = Ident.repr_ident
 let make_ident = Ident.make_ident