- None -> GrafiteAst.Bydone (loc, t)
- | Some (ty,id,t1) ->
- GrafiteAst.By_term_we_proved(loc, t, ty, id, t1))
+ 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)))