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
---
 parsing/g_vernac.ml4 | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 30c88a11c0..81bd6a1084 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -138,11 +138,7 @@ GEXTEND Gram
                     | Some (SelectNth g) -> c (Some g)
                     | None -> c None
                     | _ ->
-                        (* arnaud: the error is raised bizarely:
-                           "all:Check 0." doesn't do anything, then
-                           inputing anything that ends with a period
-                           (including " .") raises the error. *)
-                        error "Typing and evaluation commands, cannot be used with the \"all:\" selector."
+                        VernacError (UserError ("",str"Typing and evaluation commands, cannot be used with the \"all:\" selector."))
                   end
       | tac = Tactic.tactic;
         use_dft_tac = [ "." -> false | "..." -> true ] ->
-- 
cgit v1.2.3