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