diff options
| author | herbelin | 2003-08-14 13:05:51 +0000 |
|---|---|---|
| committer | herbelin | 2003-08-14 13:05:51 +0000 |
| commit | e8be3a41a1e7fc40da3af95e59fe075788895052 (patch) | |
| tree | 83b2bfa103197f9e50e04b0d80bc76dcba99449f | |
| parent | 066f74a09f887a04f83345e987d5e1d6dedece12 (diff) | |
Amélioration affichage syntaxe modules
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4271 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | translate/ppvernacnew.ml | 10 |
1 files 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) |