Many changes

[helm.git] / matita / components / grafite_parser / grafiteParser.ml

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index eaf0c4c01097e10ef8aa02ec60ee202ce7cb818a..5acdf2bd0b7e93a398d3d25e98e6520be9699819 100644 (file)
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -267,10 +267,13 @@ EXTEND
          | BYC_wehaveand (id1,t1,id2,t2) ->
             G.AndElim (loc, just, t1, id1, t2, id2))
         ])
-    | 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']->
+    | 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']->
         G.NTactic (loc,[G.We_need_to_prove (loc, t, id, t1)])
+    | IDENT "or"; IDENT "equivalently"; t = tactic_term -> G.NTactic(loc,[G.BetaRewritingStep (loc,t)])
     | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t1=tactic_term ; t2 = OPT [IDENT "or"; IDENT
-    "equivalently"; t2 = tactic_term -> t2] ->
+"equivalently"; t2 = tactic_term -> t2] ->
         G.NTactic (loc,[G.Thesisbecomes(loc,t1,t2)])
     | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->  
         G.NTactic (loc,[G.We_proceed_by_cases_on (loc, t, t1)])