| C.AConstant (_, _, s, Some v, t, [], attrs) ->
begin match get_flavour ?flavour attrs with
| flavour when List.mem flavour th_flavours ->
let ast = proc_proof st v in
let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in
| C.AConstant (_, _, s, Some v, t, [], attrs) ->
begin match get_flavour ?flavour attrs with
| flavour when List.mem flavour th_flavours ->
let ast = proc_proof st v in
let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in