added translation of Set to Type0 (avoid warning)

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

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.mli b/helm/software/components/ng_kernel/nCicTypeChecker.mli
index 5dc181cde03372e3b1c32db49bbedbe62419182e..51aa6458d11845d67f75dcccadf77ff65211483a 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.mli
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.mli
@@ -29,3 +29,8 @@ 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
+