changed select so that it returns a list of pairs <number of binders crossed, term>

[helm.git] / helm / ocaml / cic / cicUtil.mli

diff --git a/helm/ocaml/cic/cicUtil.mli b/helm/ocaml/cic/cicUtil.mli
index a64a983f7c3033ca60afb792bc345fecec7e4828..60c14f8a6c03e5e0d9736a3a22c9275eda047ed0 100644 (file)
--- a/helm/ocaml/cic/cicUtil.mli
+++ b/helm/ocaml/cic/cicUtil.mli
@@ -67,8 +67,9 @@ val context_of:
     Cic.term
 
 (** select all subterms of a given term matching a given context (i.e. subtrees
-* rooted at context's holes *)
-val select: term:Cic.term -> context:Cic.term -> Cic.term list
+* rooted at context's holes. The first component is the number of binder the
+* term is below *)
+val select: term:Cic.term -> context:Cic.term -> (int * Cic.term) list
 
 (** mk_rels [howmany] [from] 
  * creates a list of [howmany] rels starting from [from] in decreasing order *)