diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-04-07 08:36:37 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-04-07 08:36:37 +0000 |
commit | fdfe1e7d6cf663e1cc901d67b7cb1a477eab196d (patch) | |
tree | e053a8b73eb6f26f22e4c7975025a6281873c17c /library | |
parent | 359398d061e7639867dd14c5af6b640027e8bcb8 (diff) |
Renommage unicite/unicity pour la v8
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3852 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
-rw-r--r-- | library/nameops.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/library/nameops.ml b/library/nameops.ml index a0f5d743d..7da029094 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -15,6 +15,7 @@ open Names (* Identifiers *) let translate_v7_string = function + (* ZArith *) | "double_moins_un" -> "double_minus_one" | "double_moins_deux" -> "double_minus_two" | "entier" -> "N" @@ -34,6 +35,12 @@ let translate_v7_string = function | "Un_suivi_de" -> "double_plus_one" | "Zero_suivi_de" -> "double" | "is_double_moins_un" -> "is_double_minus_one" + (* Reals *) + | s when String.length s >= 7 & + let s' = String.sub s 0 7 in + (s' = "unicite" or s' = "unicity") -> + "uniqueness"^(String.sub s 7 (String.length s - 7)) + (* Default *) | x -> x let id_of_v7_string s = |