diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-15 09:47:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-15 09:47:43 +0200 |
| commit | cbd28511526dfb561017c3d27a73598f6ce5f68d (patch) | |
| tree | a8786b32433caa850e24f67ab5a3aa85f29a683a /theories/Numbers/Cyclic/Int31/Int31.v | |
| parent | 10e5883fed21f9631e1aa65adb7a7e62a529987f (diff) | |
| parent | 7402a7788b6a73bd5c0cb9078823d48e6f01a357 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'theories/Numbers/Cyclic/Int31/Int31.v')
| -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 4e28b5b90..f5e936cf0 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -19,7 +19,7 @@ Require Export DoubleType. arithmetic. In fact it is more general than that. The only reason for this use of 31 is the underlying mecanism 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 occurences + 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 dependently-typed n-ary constructions for the inductive type [int31], its constructor [I31] and any pattern matching on it. |