Wrap future goals into a module

2 files changed, 8 insertions, 8 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 11a8023ab6..d7904c56a8 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -370,8 +370,8 @@ let run_tactic env tac pr =
     (* Already solved goals are not to be counted as shelved. Nor are
       they to be marked as unresolvable. *)
     let retrieved, sigma = Evd.pop_future_goals sigma in
-    let retrieved = Evd.filter_future_goals (Evd.is_undefined sigma) retrieved in
-    let retrieved = List.rev_append retrieved.Evd.future_shelf (List.rev retrieved.Evd.future_comb) in
+    let retrieved = Evd.FutureGoals.filter (Evd.is_undefined sigma) retrieved in
+    let retrieved = List.rev_append retrieved.Evd.FutureGoals.shelf (List.rev retrieved.Evd.FutureGoals.comb) in
     let sigma = Proofview.Unsafe.mark_as_goals sigma retrieved in
     Proofview.Unsafe.tclEVARS sigma >>= fun () ->
     Proofview.tclUNIT (result,retrieved)
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 7f0fa587cd..51d6c923b6 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -74,14 +74,14 @@ let generic_refine ~typecheck f gl =
   (* Restore the [future goals] state. *)
   let future_goals, sigma = Evd.pop_future_goals sigma in
   (* Select the goals *)
-  let future_goals = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) future_goals in
+  let future_goals = Evd.FutureGoals.map_filter (Proofview.Unsafe.advance sigma) future_goals in
   (* Proceed to the refinement *)
   let sigma = match Proofview.Unsafe.advance sigma self with
   | None ->
     (* Nothing to do, the goal has been solved by side-effect *)
     sigma
   | Some self ->
-    match future_goals.Evd.future_principal with
+    match future_goals.Evd.FutureGoals.principal with
     | None -> Evd.define self c sigma
     | Some evk ->
         let id = Evd.evar_ident self sigma in
@@ -91,16 +91,16 @@ let generic_refine ~typecheck f gl =
         | Some id -> Evd.rename evk id sigma
   in
   (* Mark goals *)
-  let sigma = Proofview.Unsafe.mark_as_goals sigma future_goals.Evd.future_comb in
-  let sigma = Proofview.Unsafe.mark_unresolvables sigma future_goals.Evd.future_shelf in
-  let comb = CList.rev_map (fun x -> Proofview.goal_with_state x state) future_goals.Evd.future_comb in
+  let sigma = Proofview.Unsafe.mark_as_goals sigma future_goals.Evd.FutureGoals.comb in
+  let sigma = Proofview.Unsafe.mark_unresolvables sigma future_goals.Evd.FutureGoals.shelf in
+  let comb = CList.rev_map (fun x -> Proofview.goal_with_state x state) future_goals.Evd.FutureGoals.comb in
   let trace env sigma = Pp.(hov 2 (str"simple refine"++spc()++
                                    Termops.Internal.print_constr_env env sigma c)) in
   Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v ->
   Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*>
   Proofview.Unsafe.tclEVARS sigma <*>
   Proofview.Unsafe.tclSETGOALS comb <*>
-  Proofview.Unsafe.tclPUTSHELF @@ List.rev future_goals.Evd.future_shelf <*>
+  Proofview.Unsafe.tclPUTSHELF @@ List.rev future_goals.Evd.FutureGoals.shelf <*>
   Proofview.tclUNIT v
   end