Some declarative tactics did not allow the "done" option in place

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

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 5c7d31223236d3decd02fa5aa8e5a5584b8d4612..6e108ce0447109c69dab396da7faa928f1cbac89 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -55,7 +55,7 @@ let default_associativity = Gramext.NonA
 
 type by_continuation =
    BYC_done
- | BYC_weproved of CicNotationPt.term * string * CicNotationPt.term option
+ | BYC_weproved of CicNotationPt.term * string option * CicNotationPt.term option
  | BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term
  | BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term
 
@@ -263,7 +263,7 @@ EXTEND
                  (floc,CicNotationParser.Parse_error
                    "tactic_term expected here"))
               | 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 ] ; 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']->
         GrafiteAst.We_need_to_prove (loc, t, id, 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)