Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*new en G_*.ml + autres petites modifications liées à suppression du traducteur

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

5 files changed, 6 insertions, 6 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index e8faf862f5..b7d88bf026 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -483,7 +483,7 @@ let fmt_autotactic =
       (str"apply " ++ prterm c ++ str" ; trivial")
   | Unfold_nth c -> (str"unfold " ++  pr_evaluable_reference c)
   | Extern tac -> 
-      (str "(external) " ++ Pptacticnew.pr_glob_tactic (Global.env()) tac)
+      (str "(external) " ++ Pptactic.pr_glob_tactic (Global.env()) tac)
 
 let fmt_hint v =
   (fmt_autotactic v.code ++ str"(" ++ int v.pri ++ str")" ++ spc ())
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 9eed8ecd30..0c40f6b427 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -50,7 +50,7 @@ let print_rewrite_hintdb bas =
        str (if d then "rewrite -> " else "rewrite <- ") ++
        Printer.prterm c ++ str " of type " ++ Printer.prterm typ ++
        str " then use tactic " ++ 
-       Pptacticnew.pr_glob_tactic (Global.env()) t) hints)
+       Pptactic.pr_glob_tactic (Global.env()) t) hints)
  with
   Not_found -> 
    errorlabstrm "AutoRewrite" 
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 5ff27a8e95..eab475541f 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -51,7 +51,7 @@ END
 let pr_gen prc _prlc _prtac c = prc c
 
 let pr_rawc _prc _prlc _prtac raw = 
-  Ppconstrnew.pr_constr (Constrextern.extern_rawconstr Idset.empty raw)
+  Ppconstr.pr_constr (Constrextern.extern_rawconstr Idset.empty raw)
 
 let interp_raw _ _ (t,_) = t
 
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 316f3c2766..8aa5f55323 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -239,8 +239,8 @@ let prmorphism_argument_gen prrelation (variance,rel) =
 let prargument_class = prmorphism_argument_gen prrelation_class
 
 let pr_morphism_signature (l,c) =
- prlist (prmorphism_argument_gen Ppconstrnew.pr_constr) l ++
-  Ppconstrnew.pr_constr c
+ prlist (prmorphism_argument_gen Ppconstr.pr_constr) l ++
+  Ppconstr.pr_constr c
 
 let prmorphism k m =
   prterm k ++ str ": " ++
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 18b7604fb1..313ff63210 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2192,7 +2192,7 @@ let print_ltac id =
   let kn = Nametab.locate_tactic id in
   let t = lookup kn in
    str "Ltac" ++ spc() ++ pr_qualid id ++ str ":=" ++ spc() ++
-    Pptacticnew.pr_glob_tactic (Global.env ()) t
+    Pptactic.pr_glob_tactic (Global.env ()) t
  with
   Not_found ->
    errorlabstrm "print_ltac"