From da0e158cf5b012ec2b61041553ae3f871e9bef09 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 8 Dec 2009 20:06:07 +0000
Subject: Migration of ProtectedToplevel and Line_oriented_parser into new
 contrib Interface

 the ProtectedLoop feature was used only by CoqInterface.
 Idem for stuff in Line_oriented_parser

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12573 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/coq.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'ide')

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
     | _ ->
-- 
cgit v1.2.3