diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-01 22:32:56 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-01 22:32:56 +0000 |
| commit | e2701ad1e502921a960fe816e68b902469f145b9 (patch) | |
| tree | 10752a8377f51738cefd84ea8b24dfad9dbe7051 /parsing | |
| parent | 042442d818afd86881b79fc89565084f74c4929b (diff) | |
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
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/pptactic.ml | 12 |
1 files changed, 6 insertions, 6 deletions
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 |