From 1334a657052a2385c3f3b01cc65c3ccae448fa96 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Tue, 7 Jun 2016 11:47:13 -0400
Subject: CoqIDE: remove useless print

There is little point in telling the user the error report is sub optimal.

In this particular case, such error has already been reported (on
the correct location)  so reminding it in a non-localized way is not
even that bad.
---
 ide/coqOps.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 930135995..6ffe771da 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -741,7 +741,7 @@ object(self)
           self#cleanup (Doc.cut_at document to_id);
           conclusion ()
       | Fail (safe_id, loc, msg) ->
-          if loc <> None then messages#push Feedback.Error (Richpp.richpp_of_string "Fixme LOC");
+(*           if loc <> None then messages#push Feedback.Error (Richpp.richpp_of_string "Fixme LOC"); *)
           messages#push Feedback.Error msg;
           if Stateid.equal safe_id Stateid.dummy then self#show_goals
           else undo safe_id
-- 
cgit v1.2.3