diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-07 11:47:13 -0400 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-07 11:47:13 -0400 |
| commit | 1334a657052a2385c3f3b01cc65c3ccae448fa96 (patch) | |
| tree | 1712481c8883f31567ad09057750a3f24fc26138 /ide | |
| parent | 4dcd50dd2767c60f8f773fb4ca1c3d4bc68819c8 (diff) | |
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.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqOps.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |