diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/subtac/g_subtac.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4 index 89fbd6ffa4..de994d915b 100644 --- a/plugins/subtac/g_subtac.ml4 +++ b/plugins/subtac/g_subtac.ml4 @@ -52,8 +52,8 @@ GEXTEND Gram GLOBAL: subtac_gallina_loc typeclass_constraint subtac_withtac; subtac_gallina_loc: - [ [ g = Vernac.gallina -> loc, g - | g = Vernac.gallina_ext -> loc, g ] ] + [ [ Vernac.locality; g = Vernac.gallina -> loc, g + | Vernac.locality; g = Vernac.gallina_ext -> loc, g ] ] ; subtac_withtac: |