(*
    ||M||  This file is part of HELM, an Hypertextual, Electronic        
    ||A||  Library of Mathematics, developed at the Computer Science     
    ||T||  Department, University of Bologna, Italy.                     
    ||I||                                                                
    ||T||  HELM is free software; you can redistribute it and/or         
    ||A||  modify it under the terms of the GNU General Public License   
    \   /  version 2 or (at your option) any later version.      
     \ /   This software is distributed as is, NO WARRANTY.     
      V_______________________________________________________________ *)

(* $Id$ *)

(* These are the only exceptions that will be raised *)
exception TypeCheckerFailure of string Lazy.t
exception AssertFailure of string Lazy.t

val set_logger: 
  ([ `Start_type_checking of NUri.uri 
   | `Type_checking_completed of NUri.uri
   | `Type_checking_interrupted of NUri.uri
   | `Type_checking_failed of NUri.uri
   | `Trust_obj of NUri.uri
   ] -> unit) -> unit

val set_trust : (NCic.obj -> bool) -> unit

(* 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