aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/proofview.ml2
1 files changed, 1 insertions, 1 deletions
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 *)