diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-20 10:07:52 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-20 10:07:52 -0700 |
| commit | 480a4b3a79b4e4bc869daa125600655c6d2825f4 (patch) | |
| tree | 4ea0e105d0551a0b78e9627011c96bb0626ce26d /src/Util/ZUtil.v | |
| parent | 1f4bd32d809b95612ec0c1682093ca8a4ab50e91 (diff) | |
Add Z.lt_le_incl to zarith
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 5e917455b..9b487a773 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -14,7 +14,7 @@ Hint Extern 1 => lia : lia. Hint Extern 1 => lra : lra. Hint Extern 1 => nia : nia. Hint Extern 1 => omega : omega. -Hint Resolve Z.log2_nonneg Z.div_small Z.mod_small Z.pow_neg_r Z.pow_0_l Z.pow_pos_nonneg : zarith. +Hint Resolve Z.log2_nonneg Z.div_small Z.mod_small Z.pow_neg_r Z.pow_0_l Z.pow_pos_nonneg Z.lt_le_incl : zarith. Hint Resolve (fun a b H => proj1 (Z.mod_pos_bound a b H)) (fun a b H => proj2 (Z.mod_pos_bound a b H)) : zarith. (** Only hints that are always safe to apply (i.e., reversible), and |