X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicUntrusted.mli;h=702f8fc19fe5d0f31f7738b2d31aaeb306e607b8;hb=95adf6dc8e29a71adc34e71eafe3f427990126e0;hp=bb5aa304974cbebe30fcd993e7d9adb91af1fab8;hpb=c6c248e635ef35e9515ed981374ce2a0cef30e62;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicUntrusted.mli b/helm/software/components/ng_kernel/nCicUntrusted.mli
index bb5aa3049..702f8fc19 100644
--- a/helm/software/components/ng_kernel/nCicUntrusted.mli
+++ b/helm/software/components/ng_kernel/nCicUntrusted.mli
@@ -19,6 +19,7 @@ val map_obj_kind:
   ?skip_body:bool -> (NCic.term -> NCic.term) -> NCic.obj_kind -> NCic.obj_kind
 
 val metas_of_term : NCic.substitution -> NCic.context -> NCic.term -> int list
+val sort_metasenv: NCic.substitution -> NCic.metasenv -> NCic.metasenv
 
 type meta_kind = [ `IsSort | `IsType | `IsTerm ]
 val kind_of_meta: NCic.meta_attrs -> meta_kind
@@ -39,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 -> int -> NCic.term -> int