From cf5ca123b6cd64a5acd1f0524b18d3790f5fd30c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 5 Sep 2003 21:08:22 +0000
Subject: Bug affichage tactiques supplementaires en v8

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

diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 817109a97b..fbbde23037 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -362,7 +362,10 @@ let rec pr_tacarg_using_rule pr_gen = function
   | _ -> failwith "Inconsistent arguments of extended tactic"
 
 let pr_extend_gen proj prgen s l =
-  let tab = if Options.do_translate() then prtac_tab else prtac_tab_v7 in
+  let tab = 
+    if Options.do_translate() or not !Options.v7 then prtac_tab
+    else prtac_tab_v7
+  in
   try 
     let (s,pl) = proj (Hashtbl.find tab s) l in
     str s ++ pr_tacarg_using_rule prgen (pl,l)
-- 
cgit v1.2.3