summaryrefslogtreecommitdiff
path: root/theories/Numbers
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
commit2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch)
tree074182834cb406d1304aec4233718564a9c06ba1 /theories/Numbers
parent0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff)
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'theories/Numbers')
-rw-r--r--theories/Numbers/Cyclic/Int31/Int31.v2
-rw-r--r--theories/Numbers/NaryFunctions.v2
2 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index 4e28b5b9..f5e936cf 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.
diff --git a/theories/Numbers/NaryFunctions.v b/theories/Numbers/NaryFunctions.v
index 6fdf0a2a..376620dd 100644
--- a/theories/Numbers/NaryFunctions.v
+++ b/theories/Numbers/NaryFunctions.v
@@ -15,7 +15,7 @@ Require Import List.
(** * Generic dependently-typed operators about [n]-ary functions *)
(** The type of [n]-ary function: [nfun A n B] is
- [A -> ... -> A -> B] with [n] occurences of [A] in this type. *)
+ [A -> ... -> A -> B] with [n] occurrences of [A] in this type. *)
Fixpoint nfun A n B :=
match n with