diff options
Diffstat (limited to 'src/common/IntegerExtra.v')
| -rw-r--r-- | src/common/IntegerExtra.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v index 8b11823..f44cac2 100644 --- a/src/common/IntegerExtra.v +++ b/src/common/IntegerExtra.v @@ -639,7 +639,7 @@ Module IntExtra. apply unsigned_range_2. Qed. - Lemma shrx_shrx_alt_equiv : + Theorem shrx_shrx_alt_equiv : forall x y, unsigned y <= 30 -> shrx x y = shrx_alt x y. |