diff options
author | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
commit | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
tree | 591e9e512063e34099782e2518573f15ffeac003 /contrib/ring/Ring_abstract.v | |
parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
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. |