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 ++++
 1 file changed, 4 insertions(+)

(limited to 'proofs/proofview.ml')

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