Oversight in ce260a0db279ce09dda70e079ae3c35b49f05ec4 (Proper scoping of future goals).

Fixes #3757. Thanks to Hugo for helping pinpoint the issue.

1 files changed, 1 insertions, 1 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 5f2a5b786..92308d211 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 *)