From da0e158cf5b012ec2b61041553ae3f871e9bef09 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
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
---
 parsing/g_vernac.ml4 | 1 -
 1 file changed, 1 deletion(-)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 89d06d2dd..cb7507d9c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -586,7 +586,6 @@ GEXTEND Gram
 
       (* Toplevel control *)
       | IDENT "Drop" -> VernacToplevelControl Drop
-      | IDENT "ProtectedLoop" -> VernacToplevelControl ProtectedLoop
       | IDENT "Quit" -> VernacToplevelControl Quit
 
       | IDENT "Load"; verbosely = [ IDENT "Verbose" -> true | -> false ];
-- 
cgit v1.2.3