| NCicMetaSubst.MetaSubstFailure _ as exn -> fail ~exn (lazy fname)
;;
+class type g_pstatus =
+ object
+ inherit NEstatus.g_status
+ method obj: NCic.obj
+ end
+
class pstatus =
fun (o: NCic.obj) ->
- object
+ object (self)
inherit NEstatus.status
val obj = o
method obj = obj
method set_obj o = {< obj = o >}
+ method set_pstatus : 'status. #g_pstatus as 'status -> 'self
+ = fun o -> (self#set_estatus o)#set_obj o#obj
end
type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input
(* ============= move this elsewhere ====================*)
+class type ['stack] g_status =
+ object
+ inherit g_pstatus
+ method stack: 'stack
+ end
+
class ['stack] status =
fun (o: NCic.obj) (s: 'stack) ->
- object
+ object (self)
inherit (pstatus o)
val stack = s
method stack = stack
method set_stack s = {< stack = s >}
+ method set_status : 'status. 'stack #g_status as 'status -> 'self
+ = fun o -> (self#set_pstatus o)#set_stack o#stack
end
class type lowtac_status = [unit] status