From e2701ad1e502921a960fe816e68b902469f145b9 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 1 Nov 2003 22:32:56 +0000 Subject: Traduction des noms pour les refs de pr_glob_generic (via pr_global) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4760 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/pptactic.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'parsing') diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 4f6a47af5..402f7b584 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -23,7 +23,11 @@ open Pattern let pr_red_expr = Ppconstr.pr_red_expr let pr_may_eval = Ppconstr.pr_may_eval let pr_sort = Ppconstr.pr_sort -let pr_global = Ppconstr.pr_global Idset.empty +let pr_global x = + if Options.do_translate () then (* for pr_gen *) + Ppconstrnew.pr_global Idset.empty x + else + Ppconstr.pr_global Idset.empty x let pr_name = Ppconstr.pr_name let pr_opt = Ppconstr.pr_opt let pr_occurrences = Ppconstr.pr_occurrences @@ -64,10 +68,6 @@ let declare_extra_genarg_pprule for_v8 (rawwit, f) (globwit, g) (wit, h) = if for_v8 then genarg_pprule := Stringmap.add s (f,g,h) !genarg_pprule -let pi1 (a,_,_) = a -let pi2 (_,a,_) = a -let pi3 (_,_,a) = a - let pr_arg pr x = spc () ++ pr x let pr_or_var pr = function @@ -114,7 +114,7 @@ let pr_bindings prc prlc = function l | NoBindings -> mt () -let pr_with_bindings prc prlc (c,bl) = +let pr_with_bindings prc prlc (c,bl) = prc c ++ hv 0 (pr_bindings prc prlc bl) let pr_with_constr prc = function -- cgit v1.2.3