diff options
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
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 |