diff options
Diffstat (limited to 'contrib/ring/Ring_abstract.v')
-rw-r--r-- | contrib/ring/Ring_abstract.v | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v index de42e8c3..115ed5ca 100644 --- a/contrib/ring/Ring_abstract.v +++ b/contrib/ring/Ring_abstract.v @@ -6,12 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Ring_abstract.v,v 1.13.2.1 2004/07/16 19:30:13 herbelin Exp $ *) +(* $Id: Ring_abstract.v 9179 2006-09-26 12:13:06Z barras $ *) -Require Import Ring_theory. +Require Import LegacyRing_theory. Require Import Quote. Require Import Ring_normalize. +Unset Boxed Definitions. + Section abstract_semi_rings. Inductive aspolynomial : Type := @@ -127,7 +129,7 @@ Hint Resolve (SR_mult_zero_left T). Hint Resolve (SR_mult_zero_left2 T). Hint Resolve (SR_distr_left T). Hint Resolve (SR_distr_left2 T). -Hint Resolve (SR_plus_reg_left T). +(*Hint Resolve (SR_plus_reg_left T).*) Hint Resolve (SR_plus_permute T). Hint Resolve (SR_mult_permute T). Hint Resolve (SR_distr_right T). @@ -138,7 +140,7 @@ Hint Resolve (SR_plus_zero_right T). Hint Resolve (SR_plus_zero_right2 T). Hint Resolve (SR_mult_one_right T). Hint Resolve (SR_mult_one_right2 T). -Hint Resolve (SR_plus_reg_right T). +(*Hint Resolve (SR_plus_reg_right T).*) Hint Resolve refl_equal sym_equal trans_equal. (*Hints Resolve refl_eqT sym_eqT trans_eqT.*) Hint Immediate T. @@ -437,7 +439,7 @@ Hint Resolve (Th_mult_zero_left T). Hint Resolve (Th_mult_zero_left2 T). Hint Resolve (Th_distr_left T). Hint Resolve (Th_distr_left2 T). -Hint Resolve (Th_plus_reg_left T). +(*Hint Resolve (Th_plus_reg_left T).*) Hint Resolve (Th_plus_permute T). Hint Resolve (Th_mult_permute T). Hint Resolve (Th_distr_right T). @@ -447,7 +449,7 @@ Hint Resolve (Th_plus_zero_right T). Hint Resolve (Th_plus_zero_right2 T). Hint Resolve (Th_mult_one_right T). Hint Resolve (Th_mult_one_right2 T). -Hint Resolve (Th_plus_reg_right T). +(*Hint Resolve (Th_plus_reg_right T).*) Hint Resolve refl_equal sym_equal trans_equal. (*Hints Resolve refl_eqT sym_eqT trans_eqT.*) Hint Immediate T. @@ -701,4 +703,4 @@ Proof. rewrite H; reflexivity. Qed. -End abstract_rings.
\ No newline at end of file +End abstract_rings. |