From 52f4136ecf452162adb55c8de031b73c97dcdbac Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 26 Dec 2005 20:07:21 +0000
Subject: 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
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7740 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/dp/dp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'contrib/dp')

diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index b2669d317..f25794e80 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -172,7 +172,7 @@ let rec_names_for c =
        | Name id -> 
 	   let c' = Names.make_con mp dp (label_of_id id) in
 	   ignore (Global.lookup_constant c');
-	   msgnl (Ppconstrnew.pr_term (mkConst c'));
+	   msgnl (Ppconstr.pr_term (mkConst c'));
 	   c'
        | Anonymous ->
 	   raise Not_found)
-- 
cgit v1.2.3