diff options
Diffstat (limited to 'theories/Numbers/Natural/Abstract')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NBits.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v index 313b9adfd1..427a18d4ae 100644 --- a/theories/Numbers/Natural/Abstract/NBits.v +++ b/theories/Numbers/Natural/Abstract/NBits.v @@ -23,7 +23,7 @@ Module Type NBitsProp Include BoolEqualityFacts A. Ltac order_nz := try apply pow_nonzero; order'. -Hint Rewrite div_0_l mod_0_l div_1_r mod_1_r : nz. +Global Hint Rewrite div_0_l mod_0_l div_1_r mod_1_r : nz. (** Some properties of power and division *) @@ -368,7 +368,7 @@ Proof. split. apply bits_inj. intros EQ; now rewrite EQ. Qed. -Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise. +Global Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise. Tactic Notation "bitwise" "as" simple_intropattern(m) := apply bits_inj; intros m; autorewrite with bitwise. |