- GrafiteAst.Case(loc,id,params)
- | IDENT "obtain" ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None ] ; cont=rewriting_step_continuation ->
- GrafiteAst.RewritingStep(loc, Some termine, t1, t2, cont)
- | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None ] ; cont=rewriting_step_continuation ->
- GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
+ GrafiteAst.Case(loc,id,params)
+ (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
+ | IDENT "conclude";
+ termine = tactic_term;
+ SYMBOL "=" ;
+ t1=tactic_term ;
+ t2 =
+ [ IDENT "using"; t=tactic_term -> `Term t
+ | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
+ | IDENT "proof" -> `Proof
+ | params = auto_params -> `Auto params];
+ cont = rewriting_step_continuation ->
+ GrafiteAst.RewritingStep(loc, Some (None,termine), t1, t2, cont)
+ | IDENT "obtain" ; name = IDENT;
+ termine = tactic_term;
+ SYMBOL "=" ;
+ t1=tactic_term ;
+ t2 =
+ [ IDENT "using"; t=tactic_term -> `Term t
+ | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
+ | IDENT "proof" -> `Proof
+ | params = auto_params -> `Auto params];
+ cont = rewriting_step_continuation ->
+ GrafiteAst.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
+ | SYMBOL "=" ;
+ t1=tactic_term ;
+ t2 =
+ [ IDENT "using"; t=tactic_term -> `Term t
+ | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
+ | IDENT "proof" -> `Proof
+ | params = auto_params -> `Auto params];
+ cont = rewriting_step_continuation ->
+ GrafiteAst.RewritingStep(loc, None, t1, t2, cont)