diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-18 11:14:00 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-18 11:14:00 +0000 |
| commit | 58fc89afc59941f825088974b0e7aaf5d4df571a (patch) | |
| tree | 308b31dd58effc90cfcda8d04bdf69c24764c2a0 /toplevel/vernac.ml | |
| parent | 2b2c6b12076ab8d73b5d813c8ea520496f292c93 (diff) | |
Bug: faut brancher la sortie des tactiques sur stdout pendant traduction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4940 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/vernac.ml')
| -rw-r--r-- | toplevel/vernac.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index ff674bc0b..7aae0f38d 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -136,11 +136,12 @@ let post_printing loc (env,t,f,n) = function | VernacSolve (i,_,deftac) -> set_formatter_translator(); let pp = Ppvernacnew.pr_vernac_solve (i,env,t,deftac) ++ sep_end () in - if !translate_file then begin + (if !translate_file then begin msg (hov 0 (comment (fst loc) ++ pp ++ comment (snd loc - 1))); end else - msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ pp)) + msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ pp))); + Format.set_formatter_out_channel stdout | _ -> () let pr_new_syntax loc ocom = |