aboutsummaryrefslogtreecommitdiff
path: root/theories/Init
diff options
context:
space:
mode:
authorJPR2019-05-23 23:28:55 +0200
committerJPR2019-05-23 23:28:55 +0200
commitd306f5428db0d034aea55d3f0699c67c1f296cc1 (patch)
tree540bcc09ec46c8a360cda9ed7fafa9ab631d3716 /theories/Init
parent5cfdc20560392c2125dbcee31cfd308d5346b428 (diff)
Fixing typos - Part 3
Diffstat (limited to 'theories/Init')
-rw-r--r--theories/Init/Logic.v2
-rw-r--r--theories/Init/Nat.v2
2 files changed, 2 insertions, 2 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 1a391ed799..d54c8bf42d 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -37,7 +37,7 @@ Notation "~ x" := (not x) : type_scope.
Register not as core.not.type.
(** Create the "core" hint database, and set its transparent state for
- variables and constants explicitely. *)
+ variables and constants explicitly. *)
Create HintDb core.
Hint Variables Opaque : core.
diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v
index 7e7a1ced58..5952f3a31b 100644
--- a/theories/Init/Nat.v
+++ b/theories/Init/Nat.v
@@ -331,7 +331,7 @@ Definition iter (n:nat) {A} (f:A->A) (x:A) : A :=
(** Bitwise operations *)
(** We provide here some bitwise operations for unary numbers.
- Some might be really naive, they are just there for fullfiling
+ Some might be really naive, they are just there for fulfilling
the same interface as other for natural representations. As
soon as binary representations such as NArith are available,
it is clearly better to convert to/from them and use their ops.