certains id n'etaient pas renommes pour eviter les conflits avec les mots-cles

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

4 files changed, 7 insertions, 8 deletions

diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 8e7128715..ed4417797 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -23,6 +23,8 @@ open Term
 open Pattern
 (*i*)
 
+let pr_id id = Nameops.pr_id (Constrextern.v7_to_v8_id id)
+
 let sep_p = fun _ -> str"."
 let sep_v = fun _ -> str"," ++ spc()
 let sep_pp = fun _ -> str":"
@@ -124,7 +126,7 @@ let pr_opt_type_spc pr = function
 
 let pr_name = function
   | Anonymous -> str"_"
-  | Name id -> pr_id (Constrextern.v7_to_v8_id id)
+  | Name id -> pr_id id
 
 let pr_lident (b,_ as loc,id) =
   if loc <> dummy_loc then
diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli
index 51c6f8b7f..542549f74 100644
--- a/translate/ppconstrnew.mli
+++ b/translate/ppconstrnew.mli
@@ -50,6 +50,7 @@ val pr_sep_com :
   (constr_expr -> std_ppcmds) ->
   constr_expr -> std_ppcmds
 val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
+val pr_id : identifier -> std_ppcmds
 val pr_name : name -> std_ppcmds
 val pr_qualid : qualid -> std_ppcmds
 val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 2373f7371..a6ff11b0e 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -144,9 +144,8 @@ let id_of_ltac_v7_id id =
 
 let pr_ltac_or_var pr = function
   | ArgArg x -> pr x
-  | ArgVar (loc,id) -> pr_with_comments loc ( pr_id (id_of_ltac_v7_id id))
-
-let pr_id id = pr_id (Constrextern.v7_to_v8_id id)
+  | ArgVar (loc,id) ->
+      pr_with_comments loc (Nameops.pr_id (id_of_ltac_v7_id id))
 
 let pr_arg pr x = spc () ++ pr x
 
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 78d8f1bf7..41f36ccda 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -30,9 +30,6 @@ open Tacinterp
 
 let pr_spc_type = pr_sep_com spc pr_type
 
-(* Copie de Nameops *)
-let pr_id id = pr_id (Constrextern.v7_to_v8_id id)
-
 let pr_lident (b,_ as loc,id) =
   if loc <> dummy_loc then
     pr_located pr_id ((b,b+String.length(string_of_id id)),id)
@@ -42,7 +39,7 @@ let pr_lname = function
     (loc,Name id) -> pr_lident (loc,id)
   | lna -> pr_located pr_name lna
 
-let pr_ltac_id id = pr_id (id_of_ltac_v7_id id)
+let pr_ltac_id id = Nameops.pr_id (id_of_ltac_v7_id id)
 
 let pr_module r =
   let update_ref s = match r with