From 2b00f74f104586c8d8b205161320e850efa91268 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 6 Jan 2015 16:09:51 +0100
Subject: Fix setoid rewrite.

Because of f66b84de608830600e43f6d1a97c29226b6b58ea (Refine primitive: [unsafe] is now true by default), setoid rewrite could produce ill-typed term. Since setoid rewrite relies on the checks of refine to ensure well-typed, turned the check explicitely on with [~unsafe:false].---
 tactics/rewrite.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 9d9847ea57..08055004fd 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1477,7 +1477,7 @@ let assert_replacing id newt tac =
           else decl :: nc')
         env ~init:[]
     in
-    Proofview.Refine.refine begin fun sigma ->
+    Proofview.Refine.refine ~unsafe:false begin fun sigma ->
       let env' = Environ.reset_with_named_context (val_of_named_context nc') env in
       let sigma, ev = Evarutil.new_evar env' sigma concl in
       let sigma, ev' = Evarutil.new_evar env sigma newt in
@@ -1507,7 +1507,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.Unsafe.tclNEWGOALS gls in
+            let tac = Proofview.Refine.refine ~unsafe:false (fun h -> (h, p)) <*> Proofview.Unsafe.tclNEWGOALS gls in
             Proofview.Unsafe.tclEVARS undef <*>
 	    assert_replacing id newt tac
 	| Some id, None ->
@@ -1521,7 +1521,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.Unsafe.tclNEWGOALS gls
+            Proofview.Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls
             end
 	| None, None ->
             Proofview.Unsafe.tclEVARS undef <*>
-- 
cgit v1.2.3