From a5a355ec3e9cbbfa28be53b9ba6ef914136b0aba Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 21 Oct 2014 21:53:35 +0200
Subject: Proofview: move more functions to the Unsafe module.

---
 tactics/rewrite.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics')

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 <*>
-- 
cgit v1.2.3