diff options
Diffstat (limited to 'parsing/pptactic.ml')
| -rw-r--r-- | parsing/pptactic.ml | 7 |
1 files changed, 6 insertions, 1 deletions
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 () |