From 924771d6fdd1349955c2d0f500ccf34c2109507b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sun, 17 Aug 2014 19:26:58 +0200
Subject: Improving error message when applying rewrite to an expression which
 is not an equality.

---
 tactics/rewrite.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/rewrite.ml')

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index ca7fb7b0a..9102b244c 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1949,6 +1949,7 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals gl =
     let _, res = substrat (hypinfo, 0) env avoid t ty cstr evars in
     (), res
   in
+  init_setoid ();
     try
       tclWEAK_PROGRESS 
 	(tclTHEN
@@ -1965,7 +1966,6 @@ let general_s_rewrite_clause x =
     | Some id -> general_s_rewrite (Some id)
 
 let general_s_rewrite_clause x y z w ~new_goals =
-  newtactic_init_setoid () <*>
   Proofview.V82.tactic (general_s_rewrite_clause x y z w ~new_goals)
 
 let _ = Hook.set Equality.general_setoid_rewrite_clause general_s_rewrite_clause
-- 
cgit v1.2.3