diff options
| author | Enrico | 2017-04-17 20:55:26 +0200 |
|---|---|---|
| committer | GitHub | 2017-04-17 20:55:26 +0200 |
| commit | a9ec3525dd993f9d55afa897fe10bf2fc0a4b030 (patch) | |
| tree | 9b602cbabecd670d312809ff12ea3ae2f171b250 /mathcomp | |
| parent | 954284b661a7e8e01195c92388ae053108222cee (diff) | |
| parent | abf8a848e24e8cd5747be801ae940c3503cf02c0 (diff) | |
Merge pull request #120 from SkySkimmer/remove-vernacerror
Coq PR #565: G_vernac.subgoal_command is replaced by query_command
Diffstat (limited to 'mathcomp')
| -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 |