+let name_of_conj conj =
+ let mattrs,_,_ = conj in
+ let rec search_name mattrs =
+ match mattrs with
+ [] -> "Anonymous"
+ | hd::tl ->
+ match hd with
+ `Name n -> n
+ | _ -> search_name tl
+ in
+ search_name mattrs
+
+let rec loc_of_goal goal l =
+ match l with
+ [] -> fail (lazy "Reached the end")
+ | hd :: tl ->
+ let _,sw = hd in
+ let g = goal_of_switch sw in
+ if g = goal then hd
+ else loc_of_goal goal tl
+;;
+
+let has_focused_goal status =
+ match status#stack with
+ [] -> false
+ | ([],_,_,_,_) :: _tl -> false
+ | _ -> true
+;;
+
+let focus_on_case_tac case status =
+ let (_,_,metasenv,_,_) = status#obj in
+ let rec goal_of_case case metasenv =
+ match metasenv with
+ [] -> fail (lazy "The given case does not exist")
+ | (goal,conj) :: tl ->
+ if name_of_conj conj = case then goal
+ else goal_of_case case tl
+ in
+ let goal_to_focus = goal_of_case case metasenv in
+ let gstatus =
+ match status#stack with
+ [] -> fail (lazy "There is nothing to prove")
+ | (g,t,k,tag,p) :: s ->
+ let loc =
+ try
+ loc_of_goal goal_to_focus t
+ with _ -> fail (lazy "The given case is not part of the current induction/cases analysis
+ context")
+ in
+ let curloc = if has_focused_goal status then
+ let goal = extract_first_goal_from_status status in
+ [loc_of_goal goal g]
+ else []
+ in
+ (((g @- curloc) @+ [loc]),(curloc @+ (t @- [loc])),k,tag,p) :: s
+ in
+ status#set_stack gstatus
+;;
+
+let case id l status =
+ let ctx = status_parameter "context" status in
+ if ctx <> "induction" && ctx <> "cases" then fail (lazy "You can't use case outside of an
+ induction/cases analysis context")
+else
+ (
+ if has_focused_goal status then fail (lazy "Finish the current case before switching")
+ else
+ (
+(*
+ let goal = extract_first_goal_from_status status in
+ let (_,_,metasenv,_,_) = status#obj in
+ let conj = NCicUtils.lookup_meta goal metasenv in
+ let name = name_of_conj conj in
+*)
+ let continuation =
+ let rec aux l =
+ match l with
+ [] -> [id_tac]
+ | (id,ty)::tl ->
+ (try_tac (assume id ("",0,ty))) :: (aux tl)
+ in
+ aux l
+ in
+(* if name = id then block_tac continuation status *)