diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index ea3400f2ea..67cf70a3bc 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -520,8 +520,6 @@ let print_toplevel_error exc = in match exc with | End_of_input -> str "Please report: End of input",None - | Vernacexpr.ProtectedLoop -> - str "ProtectedLoop not allowed by coqide!",None | Vernacexpr.Drop -> str "Drop is not allowed by coqide!",None | Vernacexpr.Quit -> str "Quit is not allowed by coqide! Use menus.",None | _ -> |