Added count_occurrences.

[helm.git] / helm / software / components / ng_kernel / nCicUntrusted.mli

diff --git a/helm/software/components/ng_kernel/nCicUntrusted.mli b/helm/software/components/ng_kernel/nCicUntrusted.mli
index cb0b54b82ef18e72451b275c3e7912989e46cbb7..01c522ba0a557eb496c70ed1433331e4a2c025f4 100644 (file)
--- a/helm/software/components/ng_kernel/nCicUntrusted.mli
+++ b/helm/software/components/ng_kernel/nCicUntrusted.mli
@@ -40,3 +40,6 @@ val apply_subst : NCic.substitution -> NCic.context -> NCic.term -> NCic.term
 val apply_subst_context : fix_projections:bool -> 
   NCic.substitution -> NCic.context -> NCic.context
 val apply_subst_metasenv : NCic.substitution -> NCic.metasenv -> NCic.metasenv
+
+val count_occurrences :
+    subst:NCic.substitution -> NCic.context -> int -> NCic.term -> int