diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-27 14:22:37 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-27 14:22:37 +0000 |
| commit | aabccf49938d5727cc1c7a53882ce1f5108bbed5 (patch) | |
| tree | 091945168595d81915b695e68a690352b22a6b22 /theories/ZArith/ZArith_base.v | |
| parent | dd866fe3894d3d7542b45fb881aa2280378b2ae4 (diff) | |
Some more cleanups (Zeven, auxiliary, Zbool, Zmisc, ZArith_base)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14241 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/ZArith_base.v')
| -rw-r--r-- | theories/ZArith/ZArith_base.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/ZArith/ZArith_base.v b/theories/ZArith/ZArith_base.v index 05df86880..8eeca3b9a 100644 --- a/theories/ZArith/ZArith_base.v +++ b/theories/ZArith/ZArith_base.v @@ -28,8 +28,8 @@ Require Export Zbool. Require Export Zmisc. Require Export Wf_Z. -Hint Resolve Zle_refl Zplus_comm Zplus_assoc Zmult_comm Zmult_assoc Zplus_0_l - Zplus_0_r Zmult_1_l Zplus_opp_l Zplus_opp_r Zmult_plus_distr_l - Zmult_plus_distr_r: zarith. +Hint Resolve Z.le_refl Z.add_comm Z.add_assoc Z.mul_comm Z.mul_assoc Z.add_0_l + Z.add_0_r Z.mul_1_l Z.add_opp_diag_l Z.add_opp_diag_r Z.mul_add_distr_l + Z.mul_add_distr_r: zarith. Require Export Zhints. |