New tactic intro. Syntax: "# n".

[helm.git] / helm / software / components / acic_procedural / proceduralTypes.ml

diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml
index 3b6afc4c31ac0d54f18d58613c583311801e199d..cb4c11d2ee6f87b10d671297b936f903a4da36a4 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralTypes.ml
+++ b/helm/software/components/acic_procedural/proceduralTypes.ml
@@ -274,12 +274,15 @@ let render_steps a = render_steps mk_dot a
 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 _
@@ -291,13 +294,11 @@ let rec count_node a = function
    | 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