diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 7239bc23b..b5d0780bd 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -136,8 +136,8 @@ GEXTEND Gram [ [ thm = thm_token; id = pidentref; bl = binders; ":"; c = lconstr; l = LIST0 [ "with"; id = pidentref; bl = binders; ":"; c = lconstr -> - (Some id,(bl,c,None)) ] -> - VernacStartTheoremProof (thm, (Some id,(bl,c,None))::l, false) + (Some id,(bl,c)) ] -> + VernacStartTheoremProof (thm, (Some id,(bl,c))::l, false) | stre = assumption_token; nl = inline; bl = assum_list -> VernacAssumption (stre, nl, bl) | (kwd,stre) = assumptions_token; nl = inline; bl = assum_list -> @@ -757,11 +757,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)] |