From efbfd8952ea2ec1d398c314e47aa92aae331db94 Mon Sep 17 00:00:00 2001 From: monate Date: Mon, 24 Feb 2003 09:38:26 +0000 Subject: *** empty log message *** git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3691 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/coq.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'ide/coq.ml') diff --git a/ide/coq.ml b/ide/coq.ml index 73345e06f..985e3a163 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -12,6 +12,9 @@ open Evd open Hipattern open Tacmach open Reductionops +open Ideutils + +let prerr_endline s = if !debug then prerr_endline s else () let output = ref (Format.formatter_of_out_channel stdout) @@ -122,7 +125,7 @@ let prepare_goal sigma g = (prepare_hyps sigma env, (env, sigma, g.evar_concl, msg (prterm_env_at_top env g.evar_concl))) -let get_curent_goals () = +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 -- cgit v1.2.3