diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-09-26 11:18:22 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-09-26 11:18:22 +0000 |
| commit | 351a500eada776832ac9b09657e42f5d6cd7210f (patch) | |
| tree | af45a745540e1154eab8955c17e03cbbe2e6b878 /contrib/ring/Ring_abstract.v | |
| parent | 5155de9ee4bd01127a57c36cebbd01c5d903d048 (diff) | |
mise a jour du nouveau ring et ajout du nouveau field, avant renommages
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/ring/Ring_abstract.v')
| -rw-r--r-- | contrib/ring/Ring_abstract.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v index 5d5046393..574c24421 100644 --- a/contrib/ring/Ring_abstract.v +++ b/contrib/ring/Ring_abstract.v @@ -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. |