+ (* Produzioni Aggiunte *)
+ | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
+ GrafiteAst.Assume (loc, id, t)
+ | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
+ GrafiteAst.Suppose (loc, t, id)
+ | IDENT "by" ; t = tactic_term ; IDENT "we" ; IDENT "proved" ; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
+ GrafiteAst.By_term_we_proved (loc, t, ty, id)
+ | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
+ GrafiteAst.We_need_to_prove (loc, t, id)
+ | IDENT "by" ; t = tactic_term ; IDENT "done" ->
+ GrafiteAst.Bydone (loc, t)