X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicInspect.mli;h=a5b79b36d475d0aca0bd741bf9b293350ef75447;hb=c76b5031700d8a06d19afb54abc81bf5d34d8242;hp=6540441014d0cdce236e806f58b0625468d2f607;hpb=89519c7b52e06304a94019dd528925300380cdc0;p=helm.git

diff --git a/helm/software/components/cic/cicInspect.mli b/helm/software/components/cic/cicInspect.mli
index 654044101..a5b79b36d 100644
--- a/helm/software/components/cic/cicInspect.mli
+++ b/helm/software/components/cic/cicInspect.mli
@@ -31,6 +31,8 @@ val get_rels_from_premise: int -> Cic.term -> S.t
 
 val get_mutinds_of_uri: UriManager.uri -> Cic.term -> S.t
 
-(* count_nodes n t returns n + the number of nodes in t *)
-(* Cic.Implict nodes are counted if ~implicit:true      *)
-val count_nodes: implicit:bool -> int -> Cic.term -> int
+(* count_nodes n t returns n + the number of nodes in t                *)
+(* implicits, metas and casts are counted if ~meta:true                *)
+(* if ~meta:false, complies with                                       *)
+(* F.Guidi: Procedural representation of CIC Proof Terms. Last version *)
+val count_nodes: meta:bool -> int -> Cic.term -> int