From d723362607c3746944f2a67ecc58601b2ab64be3 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Thu, 30 Sep 2004 11:39:17 +0000
Subject: cutrewrite does not work with relations that are not Coq-like
 equalities. Thus it does not work for setoid relations and it can replace
 setoid_replace when the user wants to specify what the relation should be.

To solve the problem this commit enables the syntax

setoid_replace E1 with E2 using relation R ...


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

(limited to 'contrib')

diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index d72ee19e2c..2f42af6b71 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -806,8 +806,8 @@ let raw_polynom th op lc gl =
 				     c'''i; ci; c'i_eq_c''i |]))))
 	      (tclTHEN 
 		 (tclORELSE
-                   (Setoid_replace.setoid_replace ci c'''i ~new_goals:[])
-                   (Setoid_replace.setoid_replace c'''i ci ~new_goals:[]))
+                   (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)))
-- 
cgit v1.2.3