From 45583eb099a5a9725db407dbdebc1df7f40b4f31 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 12 Nov 2003 19:08:17 +0000
Subject: Mise en place systeme de renommage des noms de variables liees dans
 la bibliotheque standard

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

(limited to 'parsing')

diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 4397f67695..ccda07549e 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -115,7 +115,12 @@ let pr_bindings prc prlc = function
   | NoBindings -> mt ()
 
 let pr_with_bindings prc prlc (c,bl) =
-  prc c ++ hv 0 (pr_bindings prc prlc bl)
+  if Options.do_translate () then
+    (* translator calls pr_with_bindings on rawconstr: we cast it! *)
+    let bl' = Ppconstrnew.translate_with_bindings (fst (Obj.magic c) : rawconstr) bl in
+    prc c ++ hv 0 (pr_bindings prc prlc bl')
+  else
+    prc c ++ hv 0 (pr_bindings prc prlc bl)
 
 let pr_with_constr prc = function
   | None -> mt ()
-- 
cgit v1.2.3