From a33f08f8060f99a6ccc33f049ea3c52fc028b3c0 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Wed, 29 Sep 2004 14:51:29 +0000
Subject: New syntax

 "setoid_rewrite dir term generate side conditions constr_list"

to specify a list of side conditions that must be a subset of the generated
new goals. Used to disambiguate in case of multiple set of generated
side conditions.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6157 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 9221ed68fd..d72ee19e2c 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)
-                   (Setoid_replace.setoid_replace c'''i ci))
+                   (Setoid_replace.setoid_replace ci c'''i ~new_goals:[])
+                   (Setoid_replace.setoid_replace c'''i ci ~new_goals:[]))
 		 (tclTHEN 
 		    (tclTRY (h_exact c'i_eq_c''i))
 		    tac)))
-- 
cgit v1.2.3