diff options
Diffstat (limited to 'contrib/ring/Ring_abstract.v')
-rw-r--r-- | contrib/ring/Ring_abstract.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v index c0818da8..115ed5ca 100644 --- a/contrib/ring/Ring_abstract.v +++ b/contrib/ring/Ring_abstract.v @@ -6,9 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Ring_abstract.v 6295 2004-11-12 16:40:39Z gregoire $ *) +(* $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. @@ -129,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). @@ -140,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. @@ -439,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). @@ -449,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. |