parameter sintax added to axiom statement

[helm.git] / helm / software / components / cic / cicInspect.mli

diff --git a/helm/software/components/cic/cicInspect.mli b/helm/software/components/cic/cicInspect.mli
index c4bcd8aaf060a8e54216e9faf68455f3aa2a6d79..a5b79b36d475d0aca0bd741bf9b293350ef75447 100644 (file)
--- a/helm/software/components/cic/cicInspect.mli
+++ b/helm/software/components/cic/cicInspect.mli
@@ -30,3 +30,9 @@ val overlaps: S.t -> S.t -> bool
 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                *)
+(* 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