diff options
author | 2016-10-10 10:53:51 +0200 | |
---|---|---|
committer | 2016-10-10 11:05:22 +0200 | |
commit | c70fe0c63238128a6bb98b9fa75445c4b71c7af5 (patch) | |
tree | e8a0897676d8dc4cefc6e9d4d8f0166fe6a1366b /printing/printer.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/printer.ml')
0 files changed, 0 insertions, 0 deletions