- 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)))
+ BYC_done -> GrafiteAst.Bydone (loc, just)
+ | BYC_weproved (ty,id,t1) ->
+ GrafiteAst.By_just_we_proved(loc, just, ty, id, t1)
+ | BYC_letsuchthat (id1,t1,id2,t2) ->
+ GrafiteAst.ExistsElim (loc, just, id1, t1, id2, t2)
+ | BYC_wehaveand (id1,t1,id2,t2) ->
+ GrafiteAst.AndElim (loc, just, id1, t1, id2, t2))