diff options
| author | JPR | 2019-05-23 23:28:55 +0200 |
|---|---|---|
| committer | JPR | 2019-05-23 23:28:55 +0200 |
| commit | d306f5428db0d034aea55d3f0699c67c1f296cc1 (patch) | |
| tree | 540bcc09ec46c8a360cda9ed7fafa9ab631d3716 /theories/Init | |
| parent | 5cfdc20560392c2125dbcee31cfd308d5346b428 (diff) | |
Fixing typos - Part 3
Diffstat (limited to 'theories/Init')
| -rw-r--r-- | theories/Init/Logic.v | 2 | ||||
| -rw-r--r-- | theories/Init/Nat.v | 2 |
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. |
