From 93d43cbe5de7cca744f7208797566aa4652503c7 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 22 Sep 2003 16:12:46 +0000
Subject: suite (et fin) reparation Setoid Ring

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

diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 8adaf75eb6..b927cd8cba 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -805,8 +805,7 @@ let raw_polynom th op lc gl =
 				     c'''i; ci; c'i_eq_c''i |]))))
 	      (tclTHENS 
 		 (Setoid_replace.setoid_replace ci c'''i None)
-		 [ tac;
-                   h_exact c'i_eq_c''i ])) 
+		 [ h_exact c'i_eq_c''i; tac ])) 
 	 else
            (tclORELSE
               (tclORELSE
@@ -886,7 +885,7 @@ let polynom lc gl =
 			   then 
 			     errorlabstrm "Ring :"
 			       (str" All terms must have the same type");
-			   (tclTHEN (raw_polynom th None args) (guess_equiv_tac th)) gl		   
+			   (tclTHEN (raw_polynom th None (c1::args)) (guess_equiv_tac th)) gl		   
 		     | _ -> errorlabstrm "polynom :" 
 			 (str" This goal is not an equality nor a setoid equivalence")))
     (* Elsewhere, guess the theory, check that all terms have the same type
-- 
cgit v1.2.3