* http://cs.unibo.it/helm/.
*)
-(* This is the only exception that will be raised *)
+(* These are the only exceptions that will be raised *)
exception TypeCheckerFailure of string
exception AssertFailure of string
-val typecheck : UriManager.uri -> unit
+val typecheck : UriManager.uri -> Cic.obj
(* FUNCTIONS USED ONLY IN THE TOPLEVEL *)
(* type_of_aux' metasenv context term *)
val type_of_aux':
- Cic.metasenv -> Cic.context -> Cic.term -> Cic.term
+ ?subst:Cic.substitution -> Cic.metasenv -> Cic.context -> Cic.term -> Cic.term
(* typecheck_mutual_inductive_defs uri (itl,params,indparamsno) *)
val typecheck_mutual_inductive_defs :