diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 011565d86..3438635cf 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -756,11 +756,6 @@ GEXTEND Gram implicit_status = MaximallyImplicit}) items ] ]; - name_or_bang: [ - [ b = OPT "!"; id = name -> - not (Option.is_empty b), id - ] - ]; (* Same as [argument_spec_block], but with only implicit status and names *) more_implicits_block: [ [ name = name -> [(snd name, Vernacexpr.NotImplicit)] |