diff options
| author | Arnaud Spiwack | 2016-10-10 10:53:51 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-10-10 11:05:22 +0200 |
| commit | c70fe0c63238128a6bb98b9fa75445c4b71c7af5 (patch) | |
| tree | e8a0897676d8dc4cefc6e9d4d8f0166fe6a1366b /proofs/proofview.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 'proofs/proofview.ml')
| -rw-r--r-- | proofs/proofview.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 483f82113d..ae7e2b79a8 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -1016,6 +1016,10 @@ module Goal = struct in tclUNIT (CList.map_filter map step.comb) + let unsolved { self=self } = + tclEVARMAP >>= fun sigma -> + tclUNIT (not (Option.is_empty (advance sigma self))) + (* compatibility *) let goal { self=self } = self |