X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.mli;h=c333430b91c02db578deaa9a959bbf06ae7fac76;hb=810bbac9ad50436ada9f2f5a9b069b3f59e079ab;hp=5dc181cde03372e3b1c32db49bbedbe62419182e;hpb=5f926fd66f345c273bc66cc3ab9b1344ad0eac25;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.mli b/helm/software/components/ng_kernel/nCicTypeChecker.mli
index 5dc181cde..c333430b9 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.mli
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.mli
@@ -29,3 +29,11 @@ exception AssertFailure of string Lazy.t
 (* typechecks the object, raising an exception if illtyped *)
 val typecheck_obj : NCic.obj -> unit
 
+val typeof: 
+  subst:NCic.substitution -> metasenv:NCic.metasenv -> 
+  NCic.context -> NCic.term -> 
+    NCic.term
+
+val set_logger: 
+  ([ `Start_type_checking of NUri.uri 
+   | `Type_checking_completed of NUri.uri ] -> unit) -> unit