diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2019-03-25 11:02:25 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2019-03-25 11:02:25 +0100 |
| commit | 8c1735389e54d6ed4d8552a9e3f568d5edc5fa72 (patch) | |
| tree | 382e2e48bab10bc44e1d3c7a03ca4aff28f09073 /backend/RTLgenproof.v | |
| parent | 02015cafba394b4e18c6231204c5838724b31297 (diff) | |
| download | compcert-kvx-8c1735389e54d6ed4d8552a9e3f568d5edc5fa72.tar.gz compcert-kvx-8c1735389e54d6ed4d8552a9e3f568d5edc5fa72.zip | |
Integers.v: add modulus_gt_one (#259)
Since the number of bits is > 0, it is guaranteed that
modulus > 1, not just that modulus > 0.
(Suggested by Jake Waksbaum @jbaum.)
Diffstat (limited to 'backend/RTLgenproof.v')
0 files changed, 0 insertions, 0 deletions