(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
-exception Error of string lazy_t
-val fail: string lazy_t -> 'a
+exception Error of string lazy_t * exn option
+val fail: ?exn:exn -> string lazy_t -> 'a
class pstatus :
NCic.obj ->
'status * cic_term * cic_term (* status, term, type *)
val apply_subst:
#pstatus as 'status -> NCic.context -> cic_term -> 'status * cic_term
+val fix_sorts: cic_term -> cic_term
val get_goalty: #pstatus -> int -> cic_term
val mk_meta:
val mk_out_scope:
int -> (#pstatus as 'status) -> cic_term -> 'status * cic_term
-val pp_tac_status: #pstatus -> unit
+val pp_status: #pstatus -> unit
class ['stack] status :
NCic.obj -> 'stack ->