From abf8a848e24e8cd5747be801ae940c3503cf02c0 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Mon, 17 Apr 2017 14:30:14 +0200
Subject: Coq PR #565: G_vernac.subgoal_command is replaced by query_command

---
 mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'mathcomp/ssreflect/plugin/trunk')

diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
index b6ba5ec..b5c54dc 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
@@ -1748,9 +1748,9 @@ GEXTEND Gram
     | "*"; tac = ssrtclarg -> ssrtac_expr !@loc "tclstar" [gen_tclarg tac] 
     ] ];
   tactic_mode: [
-    [ "+"; tac = G_vernac.subgoal_command -> tac None
-    | "-"; tac = G_vernac.subgoal_command -> tac None
-    | "*"; tac = G_vernac.subgoal_command -> tac None
+    [ "+"; tac = G_vernac.query_command -> tac None
+    | "-"; tac = G_vernac.query_command -> tac None
+    | "*"; tac = G_vernac.query_command -> tac None
     ] ];
 END
 
-- 
cgit v1.2.3