From 93c7fc0e58c8d510392b6ef95d9196e92925edb4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 22 Nov 2014 14:12:02 +0100
Subject: In setoid_rewrite error messages: - removed the encapsulation in a
 Tactic Failure (I don't see why   setoid_rewrite should specifically raise a
 Fail - do I miss something?) - avoid having twice a "Unable to satisfy ...
 constraints" message.

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

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 49c0a81eb1..3afb654d81 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1540,23 +1540,24 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
       beta <*> Proofview.shelve_unifiable
     with
     | PretypeError (env, evd, (UnsatisfiableConstraints _ as e)) ->
-      raise (RewriteFailure (str"Unable to satisfy the rewriting constraints."
-			     ++ fnl () ++ Himsg.explain_pretype_error env evd e))
+      raise (RewriteFailure (Himsg.explain_pretype_error env evd e))
   end
 
 let tactic_init_setoid () = 
   try init_setoid (); tclIDTAC
   with e when Errors.noncritical e -> tclFAIL 0 (str"Setoid library not loaded")
 
+(** Setoid rewriting when called with "rewrite_strat" *)
 let cl_rewrite_clause_strat strat clause =
   tclTHEN (tactic_init_setoid ())
   (fun gl -> 
      try Proofview.V82.of_tactic (cl_rewrite_clause_newtac strat clause) gl
      with RewriteFailure e ->
-       tclFAIL 0 (str"setoid rewrite failed: " ++ e) gl
+       errorlabstrm "" (str"setoid rewrite failed: " ++ e)
      | Refiner.FailError (n, pp) -> 
        tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp) gl)
 
+(** Setoid rewriting when called with "setoid_rewrite" *)
 let cl_rewrite_clause l left2right occs clause gl =
   let strat = rewrite_with left2right (general_rewrite_unif_flags ()) l occs in
     cl_rewrite_clause_strat strat clause gl
-- 
cgit v1.2.3