diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq.ml | 12 | ||||
| -rw-r--r-- | ide/coq.mli | 2 | ||||
| -rw-r--r-- | ide/coqide.ml | 5 |
3 files changed, 4 insertions, 15 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index 7f27d3b9f0..fbb8759d1b 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -514,23 +514,15 @@ let get_current_pm_goal () = let gl = sig_it gls in prepare_goal sigma gl - let get_current_goals () = let pfts = get_pftreestate () in let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in let sigma = Tacmach.evc_of_pftreestate pfts in List.map (prepare_goal sigma) gls -let get_current_goals_nb () = - try List.length (get_current_goals ()) with _ -> 0 - let print_no_goal () = - let pfts = get_pftreestate () in - let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in - assert (gls = []); - let sigma = Tacmach.project (Tacmach.top_goal_of_pftreestate pfts) in - msg (Printer.pr_subgoals (Decl_mode.get_end_command pfts) sigma gls) - + (* Fall back on standard coq goal printer for completed goal printing *) + msg (pr_open_subgoals ()) let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) = [("clear "^ident),("clear "^ident^"."); diff --git a/ide/coq.mli b/ide/coq.mli index d9b27811e7..7ee95a4004 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -65,8 +65,6 @@ val get_current_goals : unit -> goal list val get_current_pm_goal : unit -> goal -val get_current_goals_nb : unit -> int - val print_no_goal : unit -> string val process_exn : exn -> string*(Util.loc option) diff --git a/ide/coqide.ml b/ide/coqide.ml index 7ba267c31f..14a0fd0371 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -769,7 +769,7 @@ object(self) try proof_buffer#set_text ""; match Decl_mode.get_current_mode () with - Decl_mode.Mode_none -> proof_buffer#insert (Coq.print_no_goal ()) + Decl_mode.Mode_none -> () | Decl_mode.Mode_tactic -> begin let s = Coq.get_current_goals () in @@ -827,8 +827,7 @@ object(self) try proof_buffer#set_text ""; match Decl_mode.get_current_mode () with - Decl_mode.Mode_none -> - proof_buffer#insert (Coq.print_no_goal ()) + Decl_mode.Mode_none -> () | Decl_mode.Mode_tactic -> begin match Coq.get_current_goals () with |