X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=054bff6215e1f64ec1b6d90813a3f7a316b88089;hb=d669da59d27e2418e65a275dc5d405237db2b93a;hp=b2fb3616f6cc216866dd7a446b614e27ca7dd39c;hpb=9fce3bebddf47429f6fcab726f11dafbf3295749;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index b2fb3616f..054bff621 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -269,6 +269,8 @@ EXTEND
               | LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2)))
     | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id ] ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']->
         GrafiteAst.We_need_to_prove (loc, t, id, t1)
+    | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->  
+        GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
     | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->  
         GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
     | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->