From e8be3a41a1e7fc40da3af95e59fe075788895052 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 14 Aug 2003 13:05:51 +0000
Subject: Amélioration affichage syntaxe modules

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

diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index c0d57c5b6d..8f17a9f0fe 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -240,9 +240,9 @@ let pr_with_declaration pr_c = function
       pr_located pr_qualid qid
 
 let rec pr_module_type pr_c = function
-  | CMTEident qid -> pr_located pr_qualid qid
+  | CMTEident qid -> spc () ++ pr_located pr_qualid qid
   | CMTEwith (mty,decl) ->
-      pr_module_type pr_c mty ++ spc() ++ str" with" ++ spc() ++
+      pr_module_type pr_c mty ++ spc() ++ str"with" ++ spc() ++
       pr_with_declaration pr_c decl
 
 let pr_of_module_type prc (mty,b) =
@@ -865,17 +865,17 @@ pr_vbinders bl ++ spc())
 
   (* Modules and Module Types *)
   | VernacDefineModule (m,bl,ty,bd) ->
-      hov 2 (str"Module " ++ pr_id m ++ spc() ++
+      hov 2 (str"Module " ++ pr_id m ++
              pr_module_binders_list bl pr_lconstr ++
              pr_opt (pr_of_module_type pr_lconstr) ty ++
              pr_opt (fun me -> str ":= " ++ pr_module_expr me) bd)
   | VernacDeclareModule (id,l,m1,m2) ->
-      hov 2 (str"Declare Module " ++ pr_id id ++ spc() ++
+      hov 2 (str"Declare Module " ++ pr_id id ++
              pr_module_binders_list l pr_lconstr ++
              pr_opt (pr_of_module_type pr_lconstr) m1 ++
              pr_opt (fun me -> str ":= " ++ pr_module_expr me) m2)
   | VernacDeclareModuleType (id,l,m) ->
-      hov 2 (str"Module Type " ++ pr_id id ++ spc() ++
+      hov 2 (str"Module Type " ++ pr_id id ++
              pr_module_binders_list l pr_lconstr ++
              pr_opt (fun mt -> str ":= " ++ pr_module_type pr_lconstr mt) m)
 
-- 
cgit v1.2.3