From 07569af8e7528fc63b93824edd5253e8a92fc2c0 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Sat, 2 Nov 2013 15:36:45 +0000
Subject: Fixes parsing of all: followed by a typechecking/evaluation command.

Exceptions raised during parsing are caught by the parser and result in weird
parsing behaviour. Instead I added a special case in vernac_expr which always
raises an error.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16988 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 intf/vernacexpr.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 2f76df0e5b..8bf65d0445 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -263,6 +263,7 @@ type vernac_expr =
   | VernacTime of vernac_expr
   | VernacTimeout of int * vernac_expr
   | VernacFail of vernac_expr
+  | VernacError of exn (* always fails *)
 
   (* Syntax *)
   | VernacTacticNotation of
-- 
cgit v1.2.3