]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite/grafiteAstPp.ml
fixed some pp stuff
[helm.git] / helm / software / components / grafite / grafiteAstPp.ml
index 6b618c6ac46ad7c2efcc00e75ffedb031147f721..412fd57d5d67b965153294508be658f2979d9cfc 100644 (file)
@@ -168,7 +168,7 @@ let pp_macro ~term_pp =
   (* Whelp *)
   | WInstance (_, term) -> "whelp instance " ^ term_pp term
   | WHint (_, t) -> "whelp hint " ^ term_pp t
-  | WLocate (_, s) -> "whelp locate " ^ s
+  | WLocate (_, s) -> "whelp locate \"" ^ s ^ "\""
   | WElim (_, t) -> "whelp elim " ^ term_pp t
   | WMatch (_, term) -> "whelp match " ^ term_pp term
   (* real macros *)
@@ -258,5 +258,5 @@ let pp_comment ~term_pp ~lazy_term_pp ~obj_pp =
 
 let pp_statement ~term_pp ~lazy_term_pp ~obj_pp =
   function
-  | Executable (_, ex) -> pp_executable ~lazy_term_pp ~term_pp ~obj_pp ex
+  | Executable (_, ex) -> pp_executable ~lazy_term_pp ~term_pp ~obj_pp ex ^ "."
   | Comment (_, c) -> pp_comment ~term_pp ~lazy_term_pp ~obj_pp c