From 34815f0c8fae4c87798b18f7343c1f1afc3056eb Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 27 Nov 2014 09:28:09 +0100
Subject: Tactic primitives: missing [advance] lead to spurious dangling goals.

Closes #3801.---
 proofs/proofview.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index c850211387..15110a67c9 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -408,7 +408,8 @@ let iter_goal i =
         i goal >>
         Proof.map (fun comb -> comb :: subgoals) Comb.get
   end [] initial >>= fun subgoals ->
-  Comb.set (CList.flatten (CList.rev subgoals))
+  Solution.get >>= fun evd ->
+  Comb.set CList.(undefined evd (flatten (rev subgoals)))
 
 (** A variant of [Monad.List.fold_left2] where the first list is the
     list of focused goals. The argument tactic is executed in a focus
@@ -431,7 +432,8 @@ let fold_left2_goal i s l =
         i goal a r >>= fun r ->
         Proof.map (fun comb -> (r, comb :: subgoals)) Comb.get
   end (s,[]) initial.comb l >>= fun (r,subgoals) ->
-  Comb.set (CList.flatten (CList.rev subgoals)) >>
+  Solution.get >>= fun evd ->
+  Comb.set CList.(undefined evd (flatten (rev subgoals))) >>
   return r
 
 (** Dispatch tacticals are used to apply a different tactic to each
@@ -1060,6 +1062,7 @@ module V82 = struct
       in
       let (goalss,evd) = Evd.Monad.List.map tac initgoals initevd in
       let sgs = CList.flatten goalss in
+      let sgs = undefined evd sgs in
       InfoL.leaf (Info.Tactic (fun () -> Pp.str"<unknown>")) >>
       Pv.set { solution = evd; comb = sgs; }
     with e when catchable_exception e ->
-- 
cgit v1.2.3