From ecfd80a0521706f9f20f2ebe147f6aaed4fef43e Mon Sep 17 00:00:00 2001
From: clrenard
Date: Thu, 22 Jul 2004 13:00:29 +0000
Subject: correction d'un bug de la tactique pour les semi setoid rings.

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

diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 76e572cdd9..c15077a944 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -705,10 +705,10 @@ let build_setspolynom gl th lc =
 			       th.th_eq; p |])) |]),
 	mkLApp(coq_setspolynomial_simplify_ok,
 	       [| th.th_a; (unbox th.th_equiv); th.th_plus;
-                  th.th_mult; th.th_one; th.th_zero; th.th_eq; v;
-                  th.th_t; (unbox th.th_setoid_th);
+                  th.th_mult; th.th_one; th.th_zero; th.th_eq;
+                  (unbox th.th_setoid_th);
 		  (unbox th.th_morph).plusm;
-                  (unbox th.th_morph).multm; p |])))
+                  (unbox th.th_morph).multm; v; th.th_t; p |])))
     lp
 
 module SectionPathSet =
-- 
cgit v1.2.3