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
---
 printing/ppvernac.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 5345d40e2f..441e362b15 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -538,6 +538,7 @@ let rec pr_vernac = function
   | VernacTime v -> str"Time" ++ spc() ++ pr_vernac v
   | VernacTimeout(n,v) -> str"Timeout " ++ int n ++ spc() ++ pr_vernac v
   | VernacFail v -> str"Fail" ++ spc() ++ pr_vernac v
+  | VernacError _ -> str"No-parsing-rule for VernacError"
 
   (* Syntax *)
   | VernacTacticNotation (n,r,e) ->
-- 
cgit v1.2.3