From 44cbc3eb3574898e541e27bc4ec11bc8848a802c Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Thu, 11 Jan 2001 16:28:18 +0000
Subject: Many unuseful rewritings are no more done by Ring.

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

diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index aa7b305c09..3ce270a054 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -556,15 +556,13 @@ let raw_polynom th op lc gl =
   let polynom_tac = 
     List.fold_right2 
       (fun ci (c'i, c''i, c'i_eq_c''i) tac ->
+        let c'''i = pf_nf gl c''i in
 	 tclTHENS 
-	   (elim_type (mkAppA [| Lazy.force coq_eqT; th.th_a; c'i; ci |]))
-	   [ tclTHENS 
-	       (elim_type 
-		  (mkAppA [| Lazy.force coq_eqT; th.th_a; c''i; c'i |]))
-	       [ tac;
-		 h_exact c'i_eq_c''i ];
-	     h_reflexivity])
-      lc ltriplets polynom_unfold_tac 
+	   (elim_type (mkAppA [| Lazy.force coq_eqT; th.th_a; c'''i; ci |]))
+           [ tac ;
+             h_exact c'i_eq_c''i
+           ]
+      ) lc ltriplets polynom_unfold_tac 
   in
   polynom_tac gl
 
-- 
cgit v1.2.3