From c2bdd1d3145556423621223694bd9fb23fe86a64 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 22 Oct 2014 13:42:36 +0200
Subject: Oversight in ce260a0db279ce09dda70e079ae3c35b49f05ec4 (Proper scoping
 of future goals).

Fixes #3757. Thanks to Hugo for helping pinpoint the issue.---
 proofs/proofview.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 5f2a5b7865..92308d2111 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -935,7 +935,7 @@ struct
     (** Select the goals *)
     let comb = undefined sigma (CList.rev evs) in
     let sigma = CList.fold_left mark_as_goal sigma comb in
-    Pv.set { solution = Evd.reset_future_goals sigma; comb; }
+    Pv.set { solution = sigma; comb; }
   end
 
   (** Useful definitions *)
-- 
cgit v1.2.3