- GrafiteAst.Case(loc,id,params)
- | IDENT "let" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ; IDENT "such" ; IDENT "that" ; t1=tactic_term ->
- GrafiteAst.Let1 (loc, id, t, t1)
- | IDENT "by" ; t=[t'=tactic_term->Some t'|SYMBOL "_"-> None] ; IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id=IDENT ; RPAREN ; IDENT "and" ; t2=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ->
- GrafiteAst.Bywehave (loc, t, t1, id, t2, id1)
- | IDENT "obtain" ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None ] ->
- GrafiteAst.RewritingStep(loc, Some termine, t1, t2)
- | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None ] ->
- GrafiteAst.RewritingStep(loc, None, t1, t2)
+ 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)