diff options
Diffstat (limited to 'ide/wg_Command.ml')
| -rw-r--r-- | ide/wg_Command.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index 931572da2..11249578e 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -119,7 +119,7 @@ object(self) let answer = match Coq.interp handle insert ~raw:true phrase with | Interface.Fail (l,str) -> "Error while interpreting "^phrase^":\n"^str - | Interface.Good results -> + | Interface.Good results | Interface.Unsafe results -> "Result for command " ^ phrase ^ ":\n" ^ results in result#buffer#insert answer |