Goal: remove [advance] from the API.

Now [Goal] only contains a few helpers.

4 files changed, 30 insertions, 36 deletions

diff --git a/proofs/goal.ml b/proofs/goal.ml
index 7a69a6035..ee3c46f5c 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -24,27 +24,6 @@ let pr_goal e = str "GOAL:" ++ Pp.int (Evar.repr e)
 let uid e = string_of_int (Evar.repr e)
 let get_by_uid u = Evar.unsafe_of_int (int_of_string u)
 
-(* [advance sigma g] returns [Some g'] if [g'] is undefined and
-    is the current avatar of [g] (for instance [g] was changed by [clear]
-    into [g']). It returns [None] if [g] has been (partially) solved. *)
-(* spiwack: [advance] is probably performance critical, and the good
-   behaviour of its definition may depend sensitively to the actual
-   definition of [Evd.find]. Currently, [Evd.find] starts looking for
-   a value in the heap of undefined variable, which is small. Hence in
-   the most common case, where [advance] is applied to an unsolved
-   goal ([advance] is used to figure if a side effect has modified the
-   goal) it terminates quickly. *)
-let rec advance sigma g =
-  let evi = Evd.find sigma g in
-  match evi.Evd.evar_body with
-  | Evd.Evar_empty -> Some g
-  | Evd.Evar_defined v ->
-      if Option.default false (Evd.Store.get evi.Evd.evar_extra Evarutil.cleared) then
-        let (e,_) = Term.destEvar v in
-        advance sigma e
-      else
-        None
-
 (* Layer to implement v8.2 tactic engine ontop of the new architecture.
    Types are different from what they used to be due to a change of the
    internal types. *)
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 7a14848b5..03d87041c 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -20,12 +20,6 @@ val get_by_uid : string -> goal
 (* Debugging help *)
 val pr_goal : goal -> Pp.std_ppcmds
 
-(* [advance sigma g] returns [Some g'] if [g'] is undefined and 
-    is the current avatar of [g] (for instance [g] was changed by [clear]
-    into [g']). It returns [None] if [g] has been (partially) solved. *)
-val advance : Evd.evar_map -> goal -> goal option
-
-
 (* Layer to implement v8.2 tactic engine ontop of the new architecture. 
    Types are different from what they used to be due to a change of the
    internal types. *)
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
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index cdc0c5e65..cec6f0fad 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -159,8 +159,30 @@ let focus i j sp =
   let (new_comb, context) = focus_sublist i j sp.comb in
   ( { sp with comb = new_comb } , context )
 
+
+(* [advance sigma g] returns [Some g'] if [g'] is undefined and
+    is the current avatar of [g] (for instance [g] was changed by [clear]
+    into [g']). It returns [None] if [g] has been (partially) solved. *)
+(* spiwack: [advance] is probably performance critical, and the good
+   behaviour of its definition may depend sensitively to the actual
+   definition of [Evd.find]. Currently, [Evd.find] starts looking for
+   a value in the heap of undefined variable, which is small. Hence in
+   the most common case, where [advance] is applied to an unsolved
+   goal ([advance] is used to figure if a side effect has modified the
+   goal) it terminates quickly. *)
+let rec advance sigma g =
+  let evi = Evd.find sigma g in
+  match evi.Evd.evar_body with
+  | Evd.Evar_empty -> Some g
+  | Evd.Evar_defined v ->
+      if Option.default false (Evd.Store.get evi.Evd.evar_extra Evarutil.cleared) then
+        let (e,_) = Term.destEvar v in
+        advance sigma e
+      else
+        None
+
 (* Unfocuses a proofview with respect to a context. *)
-let undefined defs l = CList.map_filter (Goal.advance defs) l
+let undefined defs l = CList.map_filter (advance defs) l
 let unfocus c sp =
   { sp with comb = undefined sp.solution (unfocus_sublist c sp.comb) }
 
@@ -411,7 +433,7 @@ let on_advance g ~solved ~adv =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
   Proof.get >>= fun step ->
-  match Goal.advance step.solution g with
+  match advance step.solution g with
   | None -> solved (* If [first] has been solved by side effect: do nothing. *)
   | Some g -> adv g
 
@@ -538,7 +560,7 @@ let tclINDEPENDENT tac =
 
 let tclNEWGOALS gls =
   Proof.modify begin fun step ->
-  let map gl = Goal.advance step.solution gl in
+  let map gl = advance step.solution gl in
   let gls = List.map_filter map gls in
   { step with comb = step.comb @ gls }
   end
@@ -707,6 +729,8 @@ let check_no_dependencies =
 (* [unshelve l p] adds all the goals in [l] at the end of the focused
    goals of p *)
 let unshelve l p =
+  (* advance the goals in case of clear *)
+  let l = CList.map_filter (fun g -> advance p.solution g) l in
   { p with comb = p.comb@l }
 
 (* Gives up on the goal under focus. Reports an unsafe status. Proofs
@@ -964,7 +988,7 @@ module Goal = struct
     Proof.get >>= fun step ->
     let sigma = step.solution in
     let map goal =
-      match Goal.advance sigma goal with
+      match advance sigma goal with
       | None -> None (** ppedrot: Is this check really necessary? *)
       | Some goal ->
         let gl =