aboutsummaryrefslogtreecommitdiff
path: root/translate
diff options
context:
space:
mode:
authorbarras2003-10-11 00:20:33 +0000
committerbarras2003-10-11 00:20:33 +0000
commit2b61cb974c847669eaf24dfbf47d8615812481fb (patch)
tree114bfc378dbb08e18ab57c4072277b4dc0a5fd04 /translate
parente5164cf5448cb25d2911320469bc16e44ceae511 (diff)
mise a jour nouvelle syntaxe
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4595 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate')
-rw-r--r--translate/ppvernacnew.ml5
1 files changed, 4 insertions, 1 deletions
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index ebf6a14d08..4f94658aae 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -525,7 +525,10 @@ let rec pr_vernac = function
| VernacRestoreState s -> str"Restore State" ++ spc() ++ qsnew s
(* Control *)
- | VernacList l -> hov 2 (str"[" ++ spc() ++ prlist_with_sep (fun _ -> sep_end () ++ fnl() ) (pr_located pr_vernac) l ++ spc() ++ str"]")
+ | VernacList l ->
+ hov 2 (str"[" ++ spc() ++
+ prlist (fun v -> pr_located pr_vernac v ++ sep_end () ++ fnl()) l
+ ++ spc() ++ str"]")
| VernacLoad (f,s) -> str"Load" ++ if f then (spc() ++ str"Verbose"
++ spc()) else spc() ++ qsnew s
| VernacTime v -> str"Time" ++ spc() ++ pr_vernac v