diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index dbd2fc401..fe8f517a7 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -151,7 +151,7 @@ GEXTEND Gram l = LIST0 [ "with"; id = pidentref; bl = binders; ":"; c = lconstr -> (Some id,(bl,c)) ] -> - VernacStartTheoremProof (thm, (Some id,(bl,c))::l, false) + VernacStartTheoremProof (thm, (Some id,(bl,c))::l) | stre = assumption_token; nl = inline; bl = assum_list -> VernacAssumption (stre, nl, bl) | (kwd,stre) = assumptions_token; nl = inline; bl = assum_list -> |