From ad33d68def49ad9e5c144c76c46711c60947d8aa Mon Sep 17 00:00:00 2001
From: mohring
Date: Thu, 26 Oct 2000 12:38:27 +0000
Subject: Semi_Ring_Theory_of decommente

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@767 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/ring/Ring_theory.v | 10 +---------
 1 file changed, 1 insertion(+), 9 deletions(-)

diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v
index 09b3e5b7b3..adf55b5003 100644
--- a/contrib/ring/Ring_theory.v
+++ b/contrib/ring/Ring_theory.v
@@ -371,7 +371,6 @@ End Theory_of_rings.
 
 Implicit Arguments Off.
 
-(***TODO
 Definition Semi_Ring_Theory_of :
   (A:Type)(Aplus : A -> A -> A)(Amult : A -> A -> A)(Aone : A)
   (Azero : A)(Aopp : A -> A)(Aeq : A -> A -> bool)
@@ -379,19 +378,12 @@ Definition Semi_Ring_Theory_of :
     ->(Semi_Ring_Theory Aplus Amult Aone Azero Aeq).
 Destruct 1.
 Split; Intros; Simpl; EAuto.
-EApply (Th_mult_zero_left (Build_Ring_Theory Th_plus_sym0 Th_plus_assoc0
-  Th_mult_sym0 Th_mult_assoc0 Th_plus_zero_left0 Th_mult_one_left0
-  Th_opp_def0 Th_distr_left0 Th_eq_prop0)).
-EApply (Th_plus_reg_left (Build_Ring_Theory Th_plus_sym0 Th_plus_assoc0
-  Th_mult_sym0 Th_mult_assoc0 Th_plus_zero_left0 Th_mult_one_left0
-  Th_opp_def0 Th_distr_left0 Th_eq_prop0)) with n:=n.
-Assumption.
 Defined.
 
 (* Every ring can be viewed as a semi-ring : this property will be used
   in Abstract_polynom. *)
 Coercion Semi_Ring_Theory_of : Ring_Theory >-> Semi_Ring_Theory.
-***)
+
 
 Section product_ring.
 
-- 
cgit v1.2.3