Proofview: move more functions to the Unsafe module.

3 files changed, 21 insertions, 17 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 390ab5e878..d8a7103ec0 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -327,7 +327,7 @@ let run_tactic env tac pr =
     end
   in
   let given_up = pr.given_up@give_up in
-  let proofview = Proofview.reset_future_goals tacticced_proofview in
+  let proofview = Proofview.Unsafe.reset_future_goals tacticced_proofview in
   { pr with proofview ; shelf ; given_up },status
 
 (*** Commands ***)
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 4a83ed6d20..a84a2d34dc 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -621,13 +621,6 @@ let tclINDEPENDENT tac =
   | [_] -> tac
   | _ -> list_iter_goal () (fun _ () -> tac)
 
-let tclNEWGOALS gls =
-  Pv.modify begin fun step ->
-  let map gl = advance step.solution gl in
-  let gls = List.map_filter map gls in
-  { step with comb = step.comb @ gls }
-  end
-
 (* Equality function on goals *)
 let goal_equal evars1 gl1 evars2 gl2 =
   let evi1 = Evd.find evars1 gl1 in
@@ -861,21 +854,29 @@ let numgoals =
 let in_proofview p k =
   k p.solution
 
-let reset_future_goals p =
-  { p with solution = Evd.reset_future_goals p.solution }
-
 module Unsafe = struct
 
   (* A [Proofview.tactic] version of [Refiner.tclEVARS] *)
   let tclEVARS evd =
     Pv.modify (fun ps -> { ps with solution = evd })
 
+  let tclNEWGOALS gls =
+    Pv.modify begin fun step ->
+      let map gl = advance step.solution gl in
+      let gls = List.map_filter map gls in
+      { step with comb = step.comb @ gls }
+    end
+
   let tclEVARSADVANCE evd =
     Pv.modify (fun ps -> { solution = evd; comb = undefined evd ps.comb })
 
   let tclEVARUNIVCONTEXT ctx = 
     Pv.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx })
 
+  let reset_future_goals p =
+    { p with solution = Evd.reset_future_goals p.solution }
+
+
 end
 
 module Notations = struct
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index cb0df18532..b8179f4faa 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -252,11 +252,6 @@ val tclEFFECTS : Declareops.side_effects -> unit tactic
 (* Checks for interrupts *)
 val tclCHECKINTERRUPT : unit tactic
 
-(* [tclNEWGOALS gls] adds the goals [gls] to the ones currently being proved,
-   appending them to the list of focussed goals. If a goal is already solved,
-   it is not added. Prefer the other primitives when possible. *)
-val tclNEWGOALS : Goal.goal list -> unit tactic
-
 (* Shelves all the goals under focus. The goals are placed on the
    shelf for later use (or being solved by side-effects). *)
 val shelve : unit tactic
@@ -311,6 +306,13 @@ module Unsafe : sig
 
   (* Assumes the new evar_map does not change existing goals *)
   val tclEVARS : Evd.evar_map -> unit tactic
+
+  (* [tclNEWGOALS gls] adds the goals [gls] to the ones currently
+     being proved, appending them to the list of focussed goals. If a
+     goal is already solved, it is not added. Prefer the other
+     primitives when possible. *)
+  val tclNEWGOALS : Goal.goal list -> unit tactic
+
     
   (* Assumes the new evar_map might be solving some existing goals *)
   val tclEVARSADVANCE : Evd.evar_map -> unit tactic
@@ -318,6 +320,8 @@ module Unsafe : sig
   (* Set the evar universe context *)
   val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> unit tactic
 
+  (* Clears the future goals store in the proof. *)
+  val reset_future_goals : proofview -> proofview
 end
 
 module Monad : Monad.S with type +'a t = 'a tactic
@@ -325,7 +329,6 @@ module Monad : Monad.S with type +'a t = 'a tactic
 (*** Commands ***)
 
 val in_proofview : proofview -> (Evd.evar_map -> 'a) -> 'a
-val reset_future_goals : proofview -> proofview
 
 (* Notations for building tactics. *)
 module Notations : sig