cicInspect: now we can choose not to count the Cic.Implicit constructors

[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 e7ee2ed8dd72adcef986ecf401336a57cf981907..6540441014d0cdce236e806f58b0625468d2f607 100644 (file)
--- a/helm/software/components/cic/cicInspect.mli
+++ b/helm/software/components/cic/cicInspect.mli
@@ -32,4 +32,5 @@ 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 *)
-val count_nodes: int -> Cic.term -> int
+(* Cic.Implict nodes are counted if ~implicit:true      *)
+val count_nodes: implicit:bool -> int -> Cic.term -> int