+ 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
+ |`Proof -> `Proof
+ |`SolveWith t -> `SolveWith (text,prefix_len,t)
+ )
+ cont
+ | GrafiteAst.PrintStack (_) -> Declarative.print_stack