From 27a2b25a2ada2227edefb4302856263778c83c43 Mon Sep 17 00:00:00 2001 From: coq Date: Fri, 3 Jun 2005 13:33:33 +0000 Subject: suppression de code commente git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7103 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/coqide.ml | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/ide/coqide.ml b/ide/coqide.ml index c838cd6687..ccfbc069b1 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -953,10 +953,7 @@ object(self) full_goal_done <- false; prerr_endline "Send_to_coq starting now"; if replace then begin - let r,info = -(* full_do_if_not_computing "coq eval and replace" *) - Coq.interp_and_replace ("Info " ^ phrase) - in + let r,info = Coq.interp_and_replace ("Info " ^ phrase) in let msg = read_stdout () in self#insert_message (if show_output then msg else ""); -- cgit v1.2.3