X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Fgrafite%2FgrafiteAstPp.ml;h=d775a77dcdce83bcab4c8a018474bc7870a5bf17;hb=577e68880396ea19dc0c190435a2268540696be1;hp=0530697ada6b252b580405a4837ef7eca0e5eb68;hpb=6a25db65c9a787daf7344e3b166b2d798b1ff1a5;p=helm.git

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 0530697ad..d775a77dc 100644
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -166,6 +166,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   | By_term_we_proved (_, term, term1, ident, term2) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term)  ^ "we proved" ^ term_pp term1 ^ (match ident with None -> "" | Some ident -> "(" ^ident^ ")") ^
        (match term2 with  None -> " " | Some term2 -> term_pp term2)
   | We_need_to_prove (_, term, ident, term1) -> "we need to prove" ^ term_pp term ^ (match ident with None -> "" | Some ident -> "(" ^ ident ^ ")") ^ (match term1 with None -> " " | Some term1 -> term_pp term1)
+  | We_proceed_by_cases_on (_, term, term1) -> "we proceed by cases on" ^ term_pp term ^ "to prove" ^ term_pp term1
   | We_proceed_by_induction_on (_, term, term1) -> "we proceed by induction on" ^ term_pp term ^ "to prove" ^ term_pp term1
   | Byinduction (_, term, ident) -> "by induction hypothesis we know" ^ term_pp term ^ "(" ^ ident ^ ")"
   | Thesisbecomes (_, term) -> "the thesis becomes " ^ term_pp term