From 8fb7ef8984de20f1b6adbc5f438bd6cfcf4d1ed0 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Fri, 3 Sep 2004 09:31:04 +0000
Subject: The old implementation of (setoid_replace c1 with c2) used to replace
 either c1 with c2 or c2 with c1 (if c1 did not occur in the goal). The new
 implementation will not do it. Thus I am replacing every occurrence of
 (setoid_replace c1 with c2) with (setoid_replace c1 with c2 || setoid_replace
 c2 with c1).

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

diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 178b866de0..9221ed68fd 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -805,7 +805,9 @@ let raw_polynom th op lc gl =
                                      (unbox th.th_setoid_th);
 				     c'''i; ci; c'i_eq_c''i |]))))
 	      (tclTHEN 
-		 (Setoid_replace.setoid_replace ci c'''i)
+		 (tclORELSE
+                   (Setoid_replace.setoid_replace ci c'''i)
+                   (Setoid_replace.setoid_replace c'''i ci))
 		 (tclTHEN 
 		    (tclTRY (h_exact c'i_eq_c''i))
 		    tac)))
-- 
cgit v1.2.3