diff options
Diffstat (limited to 'contrib/ring/Ring_normalize.v')
| -rw-r--r-- | contrib/ring/Ring_normalize.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v index 7b40328a..4a082396 100644 --- a/contrib/ring/Ring_normalize.v +++ b/contrib/ring/Ring_normalize.v @@ -6,9 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Ring_normalize.v 6295 2004-11-12 16:40:39Z gregoire $ *) +(* $Id: Ring_normalize.v 9179 2006-09-26 12:13:06Z barras $ *) -Require Import Ring_theory. +Require Import LegacyRing_theory. Require Import Quote. Set Implicit Arguments. @@ -356,7 +356,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). @@ -367,7 +367,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. @@ -785,7 +785,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). @@ -796,7 +796,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. |