diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-04-28 11:25:29 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-04-28 11:25:29 +0200 |
| commit | 66a68a4329ce199f25184ba8b2d98b4679e7ddae (patch) | |
| tree | ce90c93341c58e82813da8b1a567ce6a3f3ed424 /parsing | |
| parent | 0a255f51809e8d29a7239bfbd9fe57a8b2b41705 (diff) | |
| parent | 2ddc9d12bd4616f10245c40bc0c87ae548911809 (diff) | |
Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of let-ins
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 011565d86..8f6b28f13 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 -> |