X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.mli;h=df76faab71255607b1763621d755232a79565fe2;hb=f2d96fcafce09d26d483fa18a9e6e36124a462c9;hp=6ad40b8bb555c91f1f339fcb97861918b40eb724;hpb=0542386e10041791982e7240f281299677b1997b;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.mli b/helm/software/components/ng_kernel/nCicTypeChecker.mli
index 6ad40b8bb..df76faab7 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.mli
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.mli
@@ -33,6 +33,8 @@ val typeof:
   NCic.context -> NCic.term -> 
     NCic.term
 
+val height_of_obj_kind: NUri.uri -> NCic.obj_kind -> int
+
 val get_relevance : 
   metasenv:NCic.metasenv -> subst:NCic.substitution ->
   NCic.context -> NCic.term -> NCic.term list -> bool list