Mise en place d'un traducteur de noms v7->v8

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

4 files changed, 34 insertions, 4 deletions

diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 7c49c18c2..9127f28e6 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -20,7 +20,7 @@ let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
 
 let gen_reference locstr dir s =
   let dir = make_dir ("Coq"::dir) in
-  let id = id_of_string s in
+  let id = Nameops.id_of_v7_string s in
   try 
     Nametab.absolute_reference (Libnames.make_path dir id)
   with Not_found ->
diff --git a/library/libnames.ml b/library/libnames.ml
index 4440780a5..00a28b71f 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -131,8 +131,8 @@ let repr_path { dirpath = pa; basename = id } = (pa,id)
 (* parsing and printing of section paths *)
 let string_of_path sp =
   let (sl,id) = repr_path sp in
-  if repr_dirpath sl = [] then string_of_id id
-  else (string_of_dirpath sl) ^ "." ^ (string_of_id id)
+  if repr_dirpath sl = [] then string_of_v7_id id
+  else (string_of_dirpath sl) ^ "." ^ (string_of_v7_id id)
 
 let sp_ord sp1 sp2 =
   let (p1,id1) = repr_path sp1
diff --git a/library/nameops.ml b/library/nameops.ml
index ee5bb7477..a0f5d743d 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -14,7 +14,35 @@ open Names
 
 (* Identifiers *)
 
-let pr_id id = (str (string_of_id id))
+let translate_v7_string = function 
+  | "double_moins_un" -> "double_minus_one"
+  | "double_moins_deux" -> "double_minus_two"
+  | "entier" -> "N"
+  | "SUPERIEUR" -> "GREATER"
+  | "EGAL" -> "EQUAL"
+  | "INFERIEUR" -> "LESSER"
+  | "add_un" -> "add_one"
+  | "sub_un" -> "sub_one"
+  | "convert_add_un" -> "convert_add_one"
+  | "compare_convert_INFERIEUR" -> "compare_convert_GREATER"
+  | "compare_convert_SUPERIEUR" -> "compare_convert_LESSER"
+  | "compare_convert_EGAL"      -> "compare_convert_EQUAL"
+  | "convert_compare_INFERIEUR" -> "convert_compare_GREATER"
+  | "convert_compare_SUPERIEUR" -> "convert_compare_LESSER"
+  | "convert_compare_EGAL"      -> "convert_compare_EQUAL"
+  | "Nul" -> "Null"
+  | "Un_suivi_de" -> "double_plus_one"
+  | "Zero_suivi_de" -> "double"
+  | "is_double_moins_un" -> "is_double_minus_one"
+  | x -> x
+
+let id_of_v7_string s =
+  id_of_string (if !Options.v7 then s else translate_v7_string s)
+let string_of_v7_id id =
+  let x = string_of_id id in
+  if Options.do_translate() then translate_v7_string x else x
+
+let pr_id id = str (string_of_v7_id id)
 
 let wildcard = id_of_string "_"
 
diff --git a/library/nameops.mli b/library/nameops.mli
index 1ae0c5303..9e70f0a17 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -11,6 +11,8 @@
 open Names
 
 (* Identifiers and names *)
+val id_of_v7_string : string -> identifier
+val string_of_v7_id : identifier -> string (* For v7->v8 translation *)
 val pr_id : identifier -> Pp.std_ppcmds
 val wildcard : identifier