diff options
| author | herbelin | 2006-01-11 00:15:01 +0000 |
|---|---|---|
| committer | herbelin | 2006-01-11 00:15:01 +0000 |
| commit | c1bc3bc1d4ef6e6f2ccab4ae0b58db124b39c41a (patch) | |
| tree | 9a25ccf27e664e3c3aeb10bad130c5a48b44d46c /kernel | |
| parent | ed2af181cf0f381e61a82b354449abb549b8b47b (diff) | |
Suppression résidus code v7 et traducteur
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7834 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/names.ml | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index a2c41beb75..7b83e18c3a 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -19,13 +19,7 @@ let id_ord = Pervasives.compare let id_of_string s = String.copy s -let map_ident id = - if Options.do_translate() then - match id with - "fix" -> "Fix" - | _ -> id - else id -let string_of_id id = String.copy (map_ident id) +let string_of_id id = String.copy id (* Hash-consing of identifier *) module Hident = Hashcons.Make( |