From 4bf699dc783072ee4c1e641e018474fbbf710e99 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Wed, 2 Feb 2005 21:13:43 +0000
Subject:                setoid_rewrite t; [tac]

now used in place of

           setoid_replace ... with ... ; try (exact t) ; tac

The new stricter version closes a bug reported by Pierre Letouzey on coqdev.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6661 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/ring/ring.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 1eb4783d14..876020ddaf 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -805,13 +805,13 @@ let raw_polynom th op lc gl =
 				  [| th.th_a; (unbox th.th_equiv);
                                      (unbox th.th_setoid_th);
 				     c'''i; ci; c'i_eq_c''i |]))))
-	      (tclTHEN 
+	      (tclTHENS
 		 (tclORELSE
-                   (Setoid_replace.setoid_replace None ci c'''i ~new_goals:[])
-                   (Setoid_replace.setoid_replace None c'''i ci ~new_goals:[]))
-		 (tclTHEN 
-		    (tclTRY (h_exact c'i_eq_c''i))
-		    tac)))
+                   (Setoid_replace.general_s_rewrite true c'i_eq_c''i
+                     ~new_goals:[])
+                   (Setoid_replace.general_s_rewrite false c'i_eq_c''i
+                     ~new_goals:[]))
+                 [tac]))
 	 else
            (tclORELSE
               (tclORELSE
-- 
cgit v1.2.3