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 /common/Smallstep.v | |
parent | 02015cafba394b4e18c6231204c5838724b31297 (diff) | |
download | compcert-8c1735389e54d6ed4d8552a9e3f568d5edc5fa72.tar.gz compcert-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 'common/Smallstep.v')
0 files changed, 0 insertions, 0 deletions