added generation of quick reference card of tactic syntax

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

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index ab27e853e300843a9605b8a05a1d8bb1795f69cb..9038b3b6043a198c12add0c97da8d4c9106ef38b 100644 (file)
--- 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))