diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2016-10-10 10:53:51 +0200 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2016-10-10 11:05:22 +0200 |
| commit | c70fe0c63238128a6bb98b9fa75445c4b71c7af5 (patch) | |
| tree | e8a0897676d8dc4cefc6e9d4d8f0166fe6a1366b /printing/ppvernac.ml | |
| parent | eb87cdaeb252d758b6a76b36867254823169576b (diff) | |
Fix #4416: - Incorrect "Error: Incorrect number of goals"
In `Ftactic` the number of results could desynchronise with the number
of goals when some goals were solved by side effect in a different
branch of a `DISPATCH`.
See [coq-bugs#4416](https://coq.inria.fr/bugs/show_bug.cgi?id=4416).
Diffstat (limited to 'printing/ppvernac.ml')
0 files changed, 0 insertions, 0 deletions