From adca2532e06efc6b66ed489cf1d8f778fdee2cea Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 15 Dec 2000 23:04:48 +0000 Subject: 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 --- kernel/names.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'kernel') 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 -- cgit v1.2.3