text prefix_len) (text,prefix_len,t1) id1 (text,prefix_len,t2) id2
| GrafiteAst.Thesisbecomes (_, t1, t2) -> Declarative.thesisbecomes (text,prefix_len,t1)
(match t2 with None -> None | Some t2 -> (Some (text,prefix_len,t2)))
- | GrafiteAst.RewritingStep (_,termine,t1,t2,cont) ->
- Declarative.rewritingstep (match termine with None -> None
- | Some (s,t) -> Some (s, (text,prefix_len,t)))
- (text,prefix_len,t1)
- (match t2 with
- `Term t -> just_to_tacstatus_just t2 text prefix_len
- | `Auto params -> just_to_tacstatus_just t2 text prefix_len
+ | GrafiteAst.RewritingStep (_,rhs,just,cont) ->
+ Declarative.rewritingstep (text,prefix_len,rhs)
+ (match just with
+ `Term t -> just_to_tacstatus_just just text prefix_len
+ | `Auto params -> just_to_tacstatus_just just text prefix_len
|`Proof -> `Proof
|`SolveWith t -> `SolveWith (text,prefix_len,t)
)
cont
+ | GrafiteAst.Obtain (_,id,t1) ->
+ Declarative.obtain id (text,prefix_len,t1)
+ | GrafiteAst.Conclude (_,t1) ->
+ Declarative.conclude (text,prefix_len,t1)
+ | GrafiteAst.We_proceed_by_cases_on (_, t, t1) ->
+ Declarative.we_proceed_by_cases_on (text,prefix_len,t) (text,prefix_len,t1)
+ | GrafiteAst.We_proceed_by_induction_on (_, t, t1) ->
+ Declarative.we_proceed_by_induction_on (text,prefix_len,t) (text,prefix_len,t1)
+ | GrafiteAst.Byinduction (_, t, id) -> Declarative.byinduction (text,prefix_len,t) id
+ | GrafiteAst.Case (_,id,params) -> Declarative.case id params
| GrafiteAst.PrintStack (_) -> Declarative.print_stack
in
aux aux tac (* trick for non uniform recursion call *)