diff options
Diffstat (limited to 'ide/command_windows.ml')
| -rw-r--r-- | ide/command_windows.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/ide/command_windows.ml b/ide/command_windows.ml index a351107d91..70bc4d1cd1 100644 --- a/ide/command_windows.ml +++ b/ide/command_windows.ml @@ -106,13 +106,13 @@ object(self) try result#buffer#set_text (match Coq.raw_interp coqtop phrase with - | Ide_blob.Fail (l,str) -> + | Ide_intf.Fail (l,str) -> ("Error while interpreting "^phrase^":\n"^str) - | Ide_blob.Good () -> + | Ide_intf.Good () -> match Coq.read_stdout coqtop with - | Ide_blob.Fail (l,str) -> + | Ide_intf.Fail (l,str) -> ("Error while fetching "^phrase^"results:\n"^str) - | Ide_blob.Good results -> + | Ide_intf.Good results -> ("Result for command " ^ phrase ^ ":\n" ^ results)) with e -> let (s,loc) = Coq.process_exn e in |