diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-21 15:12:21 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-21 15:12:21 +0200 |
| commit | 94e0cbc26718fe3fecc58f6f8673f5f8abb0ce31 (patch) | |
| tree | 1a62e205de6964d9cff96ae0fe3a46319206e74a /parsing | |
| parent | d30ed5fe0694466f70eed51bc689cd0fa8c00da5 (diff) | |
[vernac] Remove stale bool parameter from `VernacStartTheoremProof`
`VernacStartTheoremProof` contained a stale bool parameter from 15
years ago, which is unused today.
Diffstat (limited to 'parsing')
| -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 -> |