- | start=[IDENT "conclude" -> None | IDENT "obtain" ; name = IDENT -> Some name] ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params' -> `Auto params ] ; cont=rewriting_step_continuation ->
- GrafiteAst.RewritingStep(loc, Some (start,termine), t1, t2, cont)
- | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params' -> `Auto params ] ;
- cont=rewriting_step_continuation ->
- GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
+ | start =
+ [ IDENT "conclude" -> None
+ | IDENT "obtain" ; name = IDENT -> Some name ] ;
+ termine = tactic_term ;
+ SYMBOL "=" ;
+ t1=tactic_term ;
+ IDENT "by" ;
+ t2 =
+ [ t=tactic_term -> `Term t
+ | SYMBOL "_" ; params = auto_params' -> `Auto params
+ | IDENT "proof" -> `Proof] ;
+ cont = rewriting_step_continuation ->
+ GrafiteAst.RewritingStep(loc, Some (start,termine), t1, t2, cont)
+ | SYMBOL "=" ;
+ t1=tactic_term ;
+ IDENT "by" ;
+ t2=
+ [ t=tactic_term -> `Term t
+ | SYMBOL "_" ; params = auto_params' -> `Auto params
+ | IDENT "proof" -> `Proof] ;
+ cont=rewriting_step_continuation ->
+ GrafiteAst.RewritingStep(loc, None, t1, t2, cont)