From fdfe1e7d6cf663e1cc901d67b7cb1a477eab196d Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 7 Apr 2003 08:36:37 +0000
Subject: Renommage unicite/unicity pour la v8

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3852 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/nameops.ml | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'library')

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 =
-- 
cgit v1.2.3