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.

1 files 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