exception Error of string lazy_t * exn option
val fail: ?exn:exn -> string lazy_t -> 'a
+class type g_pstatus =
+ object
+ inherit NEstatus.g_status
+ method obj: NCic.obj
+ end
+
class pstatus :
NCic.obj ->
object ('self)
inherit NEstatus.status
method obj: NCic.obj
method set_obj: NCic.obj -> 'self
+ method set_pstatus: #g_pstatus -> 'self
end
type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input
val metas_of_term : #pstatus as 'status -> cic_term -> int list
val get_goalty: #pstatus -> int -> cic_term
+val get_subst: #pstatus -> NCic.substitution
val mk_meta:
#pstatus as 'status -> ?attrs:NCic.meta_attrs -> NCic.context ->
[ `Decl of cic_term | `Def of cic_term ] -> NCicUntrusted.meta_kind ->
val pp_status: #pstatus -> unit
+class type ['stack] g_status =
+ object
+ inherit g_pstatus
+ method stack: 'stack
+ end
+
class ['stack] status :
NCic.obj -> 'stack ->
object ('self)
inherit pstatus
method stack: 'stack
method set_stack: 'stack -> 'self
+ method set_status: 'stack #g_status -> 'self
end
class type lowtac_status = [unit] status