From c70fe0c63238128a6bb98b9fa75445c4b71c7af5 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Mon, 10 Oct 2016 10:53:51 +0200
Subject: 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).
---
 proofs/proofview.ml  | 4 ++++
 proofs/proofview.mli | 4 ++++
 2 files changed, 8 insertions(+)

(limited to 'proofs')

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
 
-- 
cgit v1.2.3