exception Error of string lazy_t * exn option
val fail: ?exn:exn -> string lazy_t -> 'a
+type automation_cache = NDiscriminationTree.DiscriminationTree.t
+type unit_eq_cache = NCicParamod.state
+
+class type g_eq_status =
+ object
+ method eq_cache : unit_eq_cache
+ end
+
+class eq_status :
+ object('self)
+ inherit g_eq_status
+ method set_eq_cache: unit_eq_cache -> 'self
+ method set_eq_status: #g_eq_status -> 'self
+ end
+
+class type g_auto_status =
+ object
+ method auto_cache : automation_cache
+ end
+
+class auto_status :
+ object('self)
+ inherit g_auto_status
+ method set_auto_cache: automation_cache -> 'self
+ method set_auto_status: #g_auto_status -> 'self
+ end
+
class type g_pstatus =
object
- inherit NEstatus.g_status
+ inherit GrafiteDisambiguate.g_status
+ inherit g_auto_status
+ inherit g_eq_status
method obj: NCic.obj
end
-class pstatus :
+class virtual pstatus :
NCic.obj ->
object ('self)
- inherit NEstatus.status
- method obj: NCic.obj
+ inherit g_pstatus
+ inherit GrafiteDisambiguate.status
+ inherit auto_status
+ inherit eq_status
method set_obj: NCic.obj -> 'self
method set_pstatus: #g_pstatus -> 'self
end
#pstatus as 'status -> ?attrs:NCic.meta_attrs -> NCic.context ->
[ `Decl of cic_term | `Def of cic_term ] -> NCicUntrusted.meta_kind ->
'status * cic_term
-val instantiate: #pstatus as 'status -> int -> cic_term -> 'status
+val instantiate: #pstatus as 'status -> ?refine:bool -> int -> cic_term -> 'status
val instantiate_with_ast: #pstatus as 'status -> int -> tactic_term -> 'status
val select_term:
method stack: 'stack
end
-class ['stack] status :
+class virtual ['stack] status :
NCic.obj -> 'stack ->
object ('self)
+ inherit ['stack] g_status
inherit pstatus
- method stack: 'stack
method set_stack: 'stack -> 'self
method set_status: 'stack #g_status -> 'self
end
-class type lowtac_status = [unit] status
+class type virtual lowtac_status = [unit] status
type 'status lowtactic = #lowtac_status as 'status -> int -> 'status
-class type tac_status = [Continuationals.Stack.t] status
+class type virtual tac_status = [Continuationals.Stack.t] status
val pp_tac_status: #tac_status -> unit