- raise FirstTypeWrong
-
-let we_need_to_prove t id t1 =
- distribute_tac (fun status goal ->
- match id with
- | None ->
- (
- match t1 with
- | None -> (* We need to prove t *)
- (
- try
- assert_tac t None status goal id_tac
- with
- | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
- )
- | Some t1 -> (* We need to prove t or equivalently t1 *)
- (
- try
- assert_tac t (Some t1) status goal (change_tac ~where:("",0,(None,[],Some Ast.UserInput)) ~with_what:t1)
- with
- | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
- | NotEquivalentTypes -> fail (lazy "The given propositions are not equivalent")
- )
- )
- | Some id ->
- (
- match t1 with
- | None -> (* We need to prove t (id) *)
- exec (block_tac [cut_tac t; branch_tac ~force:false; shift_tac; intro_tac id;
- (*merge_tac*)]) status goal
- | Some t1 -> (* We need to prove t (id) or equivalently t1 *)
- exec (block_tac [cut_tac t; branch_tac ~force:false; change_tac ~where:("",0,(None,[],Some Ast.UserInput))
- ~with_what:t1; shift_tac; intro_tac id; merge_tac]) status goal
- )
- )
+ false
+
+let bydone just status =
+ let goal = extract_first_goal_from_status status in
+ let mustdot = mustdot status in
+(*
+ let goal,mustdot =
+ let s = status#stack in
+ match s with
+ | [] -> fail (lazy "Invalid use of done")
+ | (g1, _, k, tag1) :: tl ->
+ let goals = filter_open g1 in
+ let (loc::tl) = goals in
+ let goal = goal_of_loc (loc) in
+ if List.length k > 0 then
+ goal,true
+ else
+ goal,false
+ in
+
+ *)
+(*
+ let goals = filter_open g1 in
+ let (loc::tl) = goals in
+ let goal = goal_of_loc (loc) in
+ if tag1 == `BranchTag then
+ if List.length (shift_goals s) > 0 then (* must simply shift *)
+ (
+ prerr_endline (pp status#stack);
+ prerr_endline "Head goals:";
+ List.map (fun goal -> prerr_endline (string_of_int goal)) (head_goals status#stack);
+ prerr_endline "Shift goals:";
+ List.map (fun goal -> prerr_endline (string_of_int goal)) (shift_goals status#stack);
+ prerr_endline "Open goals:";
+ List.map (fun goal -> prerr_endline (string_of_int goal)) (open_goals status#stack);
+ if tag2 == `BranchTag && g2 <> [] then
+ goal,true,false,false
+ else if tag2 == `BranchTag then
+ goal,false,true,true
+ else
+ goal,false,true,false
+ )
+ else
+ (
+ if tag2 == `BranchTag then
+ goal,false,true,true
+ else
+ goal,false,true,false
+ )
+ else
+ goal,false,false,false (* It's a strange situation, there's is an underlying level on the
+ stack but the current one was not created by a branch? Should be
+ an error *)
+ | (g, _, _, tag) :: [] ->
+ let (loc::tl) = filter_open g in
+ let goal = goal_of_loc (loc) in
+ if tag == `BranchTag then
+(* let goals = filter_open g in *)
+ goal,false,true,false
+ else
+ goal,false,false,false
+ in
+ *)
+ let l = [mk_just status goal just] in
+ let l =
+ if mustdot then List.append l [dot_tac] else l
+ in
+ (*
+ let l =
+ if mustmerge then List.append l [merge_tac] else l
+ in
+ let l =
+ if mustmergetwice then List.append l [merge_tac] else l
+ in
+ *)
+ block_tac l status
+(*
+ let (_,_,metasenv,subst,_) = status#obj in
+ let goal,last =
+ match metasenv with
+ | [] -> fail (lazy "There's nothing to prove")
+ | (_,_) :: (hd,_) :: tl -> hd,false
+ | (hd,_) :: tl -> hd,true
+ in
+ if last then
+ mk_just status goal just status
+ else
+ block_tac [ mk_just status goal just; shift_tac ] status
+*)