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 | |
| 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')
| -rw-r--r-- | proofs/proofview.ml | 4 | ||||
| -rw-r--r-- | proofs/proofview.mli | 4 |
2 files changed, 8 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 diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 2157459f46..1a367f4eac 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -466,6 +466,10 @@ module Goal : sig (** Recover the list of current goals under focus, without evar-normalization *) val goals : [ `LZ ] t tactic list tactic + (** [unsolved g] is [true] if [g] is still unsolved in the current + proof state. *) + val unsolved : 'a t -> bool tactic + (** Compatibility: avoid if possible *) val goal : [ `NF ] t -> Evar.t |