- None -> GrafiteAst.Bydone (loc, t)
- | Some (ty,id,t1) ->
- GrafiteAst.By_term_we_proved(loc, t, ty, id, t1))
- | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']->
+ BYC_done -> GrafiteAst.Bydone (loc, t')
+ | BYC_weproved (ty,id,t1) ->
+ GrafiteAst.By_term_we_proved(loc, t', ty, id, t1)
+ | BYC_letsuchthat (id1,t1,id2,t2) ->
+ (* (match t with
+ LNone floc ->
+ raise (HExtlib.Localized
+ (floc,CicNotationParser.Parse_error
+ "tactic_term expected here"))
+ | LSome t ->*) GrafiteAst.ExistsElim (loc, t', id1, t1, id2, t2)(*)*)
+ | BYC_wehaveand (id1,t1,id2,t2) ->
+ (match t with
+ LNone floc ->
+ raise (HExtlib.Localized
+ (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 -> id ] ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']->