let rec count_step a = function
| Note _
| Statement _
+ | Id _
| Qed _ -> a
| Branch (pps, _) -> List.fold_left count_steps a pps
| _ -> succ a
and count_steps a = List.fold_left count_step a
-let count = I.count_nodes ~implicit:false
+let count = I.count_nodes ~meta:false
let rec count_node a = function
| Note _