From 6c683786c8100259e8c78b710e4a75974ae00eba Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Sat, 15 Apr 2017 22:10:08 +0200
Subject: Remove VernacError

---
 plugins/ltac/g_ltac.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index ece0adb071..ca5d198c23 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -335,7 +335,7 @@ GEXTEND Gram
     |   IDENT "all"; ":" -> SelectAll ] ]
   ;
   tactic_mode:
-    [ [ g = OPT toplevel_selector; tac = G_vernac.subgoal_command -> tac g ] ]
+    [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> tac g ] ]
   ;
   command:
     [ [ IDENT "Proof"; "with"; ta = Pltac.tactic; 
-- 
cgit v1.2.3