X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite%2FgrafiteAstPp.ml;h=9038b3b6043a198c12add0c97da8d4c9106ef38b;hb=935a53fb77f36e5d90a2a59fa500744001e9d780;hp=ab27e853e300843a9605b8a05a1d8bb1795f69cb;hpb=eeca603891f29cf9d5c103b82edae0f7116cee7b;p=helm.git

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index ab27e853e..9038b3b60 100644
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -129,7 +129,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
         (match level_opt with None -> "" | Some i -> " depth = " ^ string_of_int i ^ " ")  
         (term_pp term) 
         (match terms with [] -> "" | _ -> " to " ^ terms_pp ~term_pp terms)
-        (match ident_opt with None -> "" | Some ident -> " using " ^ ident)
+        (match ident_opt with None -> "" | Some ident -> " as " ^ ident)
   | Left _ -> "left"
   | LetIn (_, term, ident) -> sprintf "let %s in %s" (term_pp term) ident
   | Reduce (_, kind, pat) ->
@@ -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))