]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite/grafiteAstPp.ml
implemented tinycals:
[helm.git] / helm / software / components / grafite / grafiteAstPp.ml
index ab27e853e300843a9605b8a05a1d8bb1795f69cb..43e2117cdb13470cb435776cd22c1420f6c68819 100644 (file)
@@ -232,7 +232,8 @@ let rec pp_tactical ~term_pp ~lazy_term_pp =
   | Semicolon _ -> ";"
   | Branch _ -> "["
   | Shift _ -> "|"
-  | Pos (_, i) -> sprintf "%d:" i
+  | Pos (_, i) -> sprintf "%s:" (String.concat "," (List.map string_of_int i))
+  | Wildcard _ -> "*:"
   | Merge _ -> "]"
   | Focus (_, goals) ->
       sprintf "focus %s" (String.concat " " (List.map string_of_int goals))