From 8e42de691475823c1ed2780bd097e9ee3202244f Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 5 Feb 2001 12:18:39 +0000
Subject: rétablissement patch Claudio

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1319 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/ring/ring.ml | 11 -----------
 1 file changed, 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
 
-- 
cgit v1.2.3