Proofview: move more functions to the Unsafe module.

5 files changed, 24 insertions, 20 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
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index ec9a9ff3e7..1e3996429b 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1477,7 +1477,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
         let gls = List.rev (Evd.fold_undefined fold undef []) in
 	match is_hyp, prf with
 	| Some id, Some p ->
-            let tac = Proofview.Refine.refine (fun h -> (h, p)) <*> Proofview.tclNEWGOALS gls in
+            let tac = Proofview.Refine.refine (fun h -> (h, p)) <*> Proofview.Unsafe.tclNEWGOALS gls in
             Proofview.Unsafe.tclEVARS undef <*>
 	    assert_replacing id newt tac
 	| Some id, None ->
@@ -1491,7 +1491,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
               let (sigma, ev) = Evarutil.new_evar env sigma newt in
               sigma, mkApp (p, [| ev |])
             in
-            Proofview.Refine.refine make <*> Proofview.tclNEWGOALS gls
+            Proofview.Refine.refine make <*> Proofview.Unsafe.tclNEWGOALS gls
             end
 	| None, None ->
             Proofview.Unsafe.tclEVARS undef <*>
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index e49857be37..60da19c186 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -307,7 +307,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
                   let init_refine =
                     Tacticals.New.tclTHENLIST [
                       Proofview.Refine.refine (fun evm -> evm, Option.get term);
-                      Proofview.tclNEWGOALS gls;
+                      Proofview.Unsafe.tclNEWGOALS gls;
                       Tactics.New.reduce_after_refine;
                     ]
                   in