| 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
with NCicUtils.Meta_not_found _ as exn -> fail ~exn (lazy "get_goalty")
;;
+let get_subst status =
+ let _,_,_,subst,_ = status#obj in subst
+;;
+
let to_subst status i entry =
let name,height,metasenv,subst,obj = status#obj in
let metasenv = List.filter (fun j,_ -> j <> i) metasenv in
let n,h,metasenv,subst,o = status#obj in
let metasenv, metano, instance, _ =
NCicMetaSubst.mk_meta ~attrs metasenv ctx ~with_type:ty kind in
+ let attrs,_,_ = NCicUtils.lookup_meta metano metasenv in
let metasenv = List.filter (fun j,_ -> j <> metano) metasenv in
let subst = (metano, (attrs, ctx, bo_, ty)) :: subst in
let status = status#set_obj (n,h,metasenv,subst,o) in
(* ============= 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