diff options
| author | Hugo Herbelin | 2018-09-24 12:05:53 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-24 12:05:53 +0200 |
| commit | a3f598cdfe681c7b0e77cbd8d9778f1920683c77 (patch) | |
| tree | efa06408e6c13c0a98b5783d2e548404474c8f98 | |
| parent | 5764e978a30c21f017741b984bc60a4f7b94faf8 (diff) | |
| parent | e186109404b665d79bf441f8d1ccee39cc76b165 (diff) | |
Merge PR #8530: Fix typo in comment.
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Int31.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index ca7d3ec074..3a2503d6b7 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -19,7 +19,7 @@ Require Export DoubleType. (** This file contains basic definitions of a 31-bit integer arithmetic. In fact it is more general than that. The only reason - for this use of 31 is the underlying mecanism for hardware-efficient + for this use of 31 is the underlying mechanism for hardware-efficient computations by A. Spiwack. Apart from this, a switch to, say, 63-bit integers is now just a matter of replacing every occurrences of 31 by 63. This is actually made possible by the use of |