+ status#set_stack gstatus
+;;
+
+let case_tac lab status =
+ let gstatus =
+ match status#stack with
+ | [] -> assert false
+ | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s
+ when is_fresh loc ->
+ let l_js =
+ List.filter
+ (fun curloc ->
+ let _,_,metasenv,_,_ = status#obj in
+ match NCicUtils.lookup_meta (goal_of_loc curloc) metasenv with
+ attrs,_,_ when List.mem (`Name lab) attrs -> true
+ | _ -> false) ([loc] @+ g') in
+ ((l_js, t , [],`BranchTag)
+ :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s)
+ | _ -> fail (lazy "can't use relative positioning here")
+ in
+ status#set_stack gstatus