rétablissement patch Claudio

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1319 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 11 deletions

diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 663390c0d4..81434acd16 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -557,7 +557,6 @@ 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
           if pf_conv_x gl c'''i ci then tac (* convertible terms *)
           else
@@ -575,16 +574,6 @@ let raw_polynom th op lc gl =
              )
            )
       ) lc ltriplets polynom_unfold_tac 
-***)
-       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 
   in
   polynom_tac gl