From f475ae32ed4ff6d4a48c6cbd94e2b6c28334ed42 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 6 Sep 2003 06:52:04 +0000
Subject: Bug affichage tactiques supplementaires en v8 (suite)

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

diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index fbbde23037..2d6e93ba29 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -120,7 +120,7 @@ let pr_bindings prc prlc = function
   | ExplicitBindings l ->
       brk (1,1) ++ str "with" ++ brk (1,1) ++ 
         prlist_with_sep spc
-          (fun b -> if Options.do_translate () then
+          (fun b -> if Options.do_translate () or not !Options.v7 then
 	    str"(" ++ pr_binding prlc b ++ str")" 
 	   else
 	    pr_binding prc b)
@@ -265,7 +265,8 @@ let rec pr_raw_generic prc prlc prtac x =
             pr_raw_generic prc prlc prtac b)
 	  x)
   | ExtraArgType s -> 
-      let tab = if Options.do_translate() then !genarg_pprule
+      let tab =
+	if Options.do_translate() or not !Options.v7 then !genarg_pprule
         else !genarg_pprule_v7 in
       try pi1 (Stringmap.find s tab) prc prtac x
       with Not_found -> str " [no printer for " ++ str s ++ str "] "
@@ -307,7 +308,8 @@ let rec pr_glob_generic prc prlc prtac x =
             pr_glob_generic prc prlc prtac b)
 	  x)
   | ExtraArgType s -> 
-      let tab = if Options.do_translate() then !genarg_pprule
+      let tab =
+	if Options.do_translate() or not !Options.v7 then !genarg_pprule
         else !genarg_pprule_v7 in
       try pi2 (Stringmap.find s tab) prc prtac x
       with Not_found -> str " [no printer for " ++ str s ++ str "] "
@@ -348,7 +350,8 @@ let rec pr_generic prc prlc prtac x =
             pr_generic prc prlc prtac b)
 	  x)
   | ExtraArgType s -> 
-      let tab = if Options.do_translate() then !genarg_pprule
+      let tab = 
+	if Options.do_translate() or not !Options.v7 then !genarg_pprule
         else !genarg_pprule_v7 in
       try pi3 (Stringmap.find s tab) prc prtac x
       with Not_found -> str " [no printer for " ++ str s ++ str "]"
-- 
cgit v1.2.3