X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicInspect.ml;h=7186fb1f1585bc901e0c3cc4a8e4f0f8aadee26b;hb=3c1a432c1612f8ed21f5b2220005599c4d9da1d5;hp=25efa4cab4108969e83b5025dc7d3fbc322c8514;hpb=89519c7b52e06304a94019dd528925300380cdc0;p=helm.git

diff --git a/helm/software/components/cic/cicInspect.ml b/helm/software/components/cic/cicInspect.ml
index 25efa4cab..7186fb1f1 100644
--- a/helm/software/components/cic/cicInspect.ml
+++ b/helm/software/components/cic/cicInspect.ml
@@ -111,12 +111,14 @@ let get_mutinds_of_uri u t =
    let g a = a in
    aux g t S.empty
 
-let count_nodes ~implicit n t =
+let count_nodes ~meta n t =
+   let offset = if meta then 1 else 0 in
    let rec aux n = function
-      | C.Implicit _                 -> if implicit then succ n else n
+      | C.Implicit _                 -> offset + n
       | C.Sort _
       | C.Rel _                      -> succ n
-      | C.Appl ts                    -> List.fold_left aux (succ n) ts
+      | C.Appl ts                    -> 
+         List.fold_left aux (List.length ts - 1 + n) ts
       | C.Const (_, ss)
       | C.MutConstruct (_, _, _, ss)
       | C.MutInd (_, _, ss)
@@ -128,18 +130,18 @@ let count_nodes ~implicit n t =
 	    | None   -> n
 	    | Some t -> aux n t
          in
-         List.fold_left map (succ n) ss
-      | C.Cast (t1, t2)
+         List.fold_left map (n + offset) ss
+      | C.Cast (t1, t2) -> aux (aux (offset + n) t2) t1
       | C.Lambda (_, t1, t2)
       | C.Prod (_, t1, t2) -> aux (aux (succ n) t2) t1
-      | C.LetIn (_, t1, ty, t2) -> aux (aux (aux (succ n) t2) ty) t1
+      | C.LetIn (_, t1, ty, t2) -> aux (aux (aux (offset + n) t2) ty) t1
       | C.MutCase (_, _, t1, t2, ss) ->
-         aux (aux (List.fold_left aux (succ n) ss) t2) t1
+         aux (aux (List.fold_left aux (offset + 1 + n) ss) t2) t1
       | C.Fix (_, ss)                ->
          let map n (_, _, t1, t2) = aux (aux n t2) t1 in
-         List.fold_left map (succ n) ss
+         List.fold_left map (2 + n) ss
       | C.CoFix (_, ss)              ->
          let map n (_, t1, t2) = aux (aux n t2) t1 in
-         List.fold_left map (succ n) ss
+         List.fold_left map (2 + n) ss
 in
 aux n t