diff options
| author | mohring | 2000-10-26 12:38:27 +0000 |
|---|---|---|
| committer | mohring | 2000-10-26 12:38:27 +0000 |
| commit | ad33d68def49ad9e5c144c76c46711c60947d8aa (patch) | |
| tree | c17a0f6cde59c0073201695ec3970083edf171da | |
| parent | daa75d5ffb8dfdf414bed31fbfe1e91718d6a5dc (diff) | |
Semi_Ring_Theory_of decommente
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@767 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/ring/Ring_theory.v | 10 |
1 files changed, 1 insertions, 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. |