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 ~meta:false
+
let rec count_node a = function
| Note _
| Inductive _
| ClearBody _ -> a
| Cut (_, t, _)
| LetIn (_, t, _)
- | Apply (t, _) -> I.count_nodes a (H.cic t)
+ | Apply (t, _) -> count a (H.cic t)
| Rewrite (_, t, _, p, _)
| Elim (t, _, p, _)
| Cases (t, p, _)
- | Change (t, _, _, p, _) ->
- let a = I.count_nodes a (H.cic t) in
- I.count_nodes a (H.cic p)
+ | Change (t, _, _, p, _) -> let a = count a (H.cic t) in count a (H.cic p)
| Branch (ss, _) -> List.fold_left count_nodes a ss
and count_nodes a = List.fold_left count_node a