]> matita.cs.unibo.it Git - helm.git/blobdiff - components/grafite/grafiteAstPp.ml
Procedural: some improvements
[helm.git] / components / grafite / grafiteAstPp.ml
index 0704863f5a779ee28282863c16b38741221ee6a6..fea47d15ba12df4e956c2ce291b778c0e2393ca7 100644 (file)
@@ -298,6 +298,7 @@ let pp_executable ~term_pp ~lazy_term_pp ~obj_pp =
                       
 let pp_comment ~term_pp ~lazy_term_pp ~obj_pp =
   function
+  | Note (_,"") -> sprintf "\n"
   | Note (_,str) -> sprintf "(* %s *)\n" str
   | Code (_,code) ->
       sprintf "(** %s. **)\n" (pp_executable ~term_pp ~lazy_term_pp ~obj_pp code)