New tactic cases (still to be documented).

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

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 840c16351f86823aeef0bc25d18acda1fcdd1b30..0530697ada6b252b580405a4837ef7eca0e5eb68 100644 (file)
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -83,6 +83,8 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
       String.concat " " 
         (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params)
   | Assumption _ -> "assumption"
+  | Cases (_, term, idents) -> sprintf "cases " ^ term_pp term ^
+      pp_intros_specs (None, idents) 
   | Change (_, where, with_what) ->
       sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what)
   | Clear (_,ids) -> sprintf "clear %s" (pp_idents ids)