From 025c4f63b28671a24bd6c46f9b23a3dad76fd179 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack <arnaud@spiwack.net>
Date: Thu, 16 Oct 2014 10:21:17 +0200
Subject: Goal: remove [advance] from the API.

Now [Goal] only contains a few helpers.
---
 proofs/proof.ml | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'proofs/proof.ml')

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 7d953d570..8ad7adc16 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -321,12 +321,9 @@ let run_tactic env tac pr =
   let (_,tacticced_proofview,(status,(to_shelve,give_up))) = Proofview.apply env tac sp in
   let shelf =
     let pre_shelf = pr.shelf@to_shelve in
-    (* Compacting immediately: if someone shelves a goal, he probably
-       expects to solve it soon. *)
+    (* avoid already to count already solved goals as shelved. *)
     Proofview.in_proofview tacticced_proofview begin fun sigma ->
-      Option.List.flatten begin
-        List.map (fun g -> Goal.advance sigma g) pre_shelf
-      end
+      List.filter (fun g -> Evd.is_undefined sigma g) pre_shelf
     end
   in
   let given_up = pr.given_up@give_up in
-- 
cgit v1.2.3