content2Procedural.ml: "Intros+LetTac" ok

[helm.git] / components / grafite / grafiteAstPp.ml

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index efc0078862b6ad3bdc43a9a33699d6e3873d8a18..0704863f5a779ee28282863c16b38741221ee6a6 100644 (file)
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -33,7 +33,7 @@ let tactical_terminator = ""
 let tactic_terminator = tactical_terminator
 let command_terminator = tactical_terminator
 
-let pp_idents idents = "[" ^ String.concat "; " idents ^ "]"
+let pp_idents idents = "(" ^ String.concat " " idents ^ ")"
 
 let pp_reduction_kind ~term_pp = function
   | `Normalize -> "normalize"
@@ -298,9 +298,9 @@ let pp_executable ~term_pp ~lazy_term_pp ~obj_pp =
                       
 let pp_comment ~term_pp ~lazy_term_pp ~obj_pp =
   function
-  | Note (_,str) -> sprintf "(* %s *)" str
+  | Note (_,str) -> sprintf "(* %s *)\n" str
   | Code (_,code) ->
-      sprintf "(** %s. **)" (pp_executable ~term_pp ~lazy_term_pp ~obj_pp code)
+      sprintf "(** %s. **)\n" (pp_executable ~term_pp ~lazy_term_pp ~obj_pp code)
 
 let pp_statement ~term_pp ~lazy_term_pp ~obj_pp =
   function