From 1e4001ca49c3902c54a98d7efea87c7b12d909fb Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 7 Oct 2003 21:15:59 +0000
Subject: Essai de traduction du contraire de 'tacledit bin/coqtop.byte' en
 'tac...'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4537 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 translate/ppvernacnew.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'translate/ppvernacnew.ml')

diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 50de4ec32..e4fa125e1 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -898,8 +898,9 @@ pr_vbinders bl ++ spc())
   | VernacSolve (i,tac,deftac) ->
       (if i = 1 then mt() else int i ++ str ": ") ++
 (*      str "By " ++*)
-      (if deftac then mt() else str "!! ") ++
       Options.with_option Options.translate_syntax (pr_raw_tactic_goal i) tac
+      ++ (if deftac & Pfedit.get_end_tac() <> None then str ".." else mt ())
+
   | VernacSolveExistential (i,c) ->
       str"Existential " ++ int i ++ pr_lconstrarg c
 
-- 
cgit v1.2.3