aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--kernel/uint31.ml8
-rw-r--r--plugins/extraction/ExtrOcamlBigIntConv.v4
-rw-r--r--plugins/extraction/ExtrOcamlNatBigInt.v2
-rw-r--r--plugins/extraction/ExtrOcamlZBigInt.v2
-rw-r--r--plugins/setoid_ring/InitialRing.v2
-rw-r--r--plugins/setoid_ring/ZArithRing.v4
-rw-r--r--theories/Logic/Hurkens.v2
7 files changed, 12 insertions, 12 deletions
diff --git a/kernel/uint31.ml b/kernel/uint31.ml
index fea12332c..3a0da2f62 100644
--- a/kernel/uint31.ml
+++ b/kernel/uint31.ml
@@ -105,15 +105,15 @@ let div21 = select div21_32 div21_64
let lt_32 x y = (x lxor 0x40000000) < (y lxor 0x40000000)
(* Do not remove the type information it is really important for
- efficiancy *)
+ efficiency *)
let lt_64 (x:int) (y:int) = x < y
let lt = select lt_32 lt_64
-(* Do not remove the type information it is really important for
- efficiancy *)
let le_32 x y =
(x lxor 0x40000000) <= (y lxor 0x40000000)
+(* Do not remove the type information it is really important for
+ efficiency *)
let le_64 (x:int) (y:int) = x <= y
let le = select le_32 le_64
@@ -121,7 +121,7 @@ let equal (x:int) (y:int) = x == y
let cmp_32 x y = Int32.compare (uint_32 x) (uint_32 y)
(* Do not remove the type information it is really important for
- efficiancy *)
+ efficiency *)
let cmp_64 (x:int) (y:int) = compare x y
let compare = select cmp_32 cmp_64
diff --git a/plugins/extraction/ExtrOcamlBigIntConv.v b/plugins/extraction/ExtrOcamlBigIntConv.v
index 265fbc52c..3a9e7cd8e 100644
--- a/plugins/extraction/ExtrOcamlBigIntConv.v
+++ b/plugins/extraction/ExtrOcamlBigIntConv.v
@@ -10,7 +10,7 @@
(** NB: The extracted code should be linked with [nums.cm(x)a]
from ocaml's stdlib and with the wrapper [big.ml] that
- simlifies the use of [Big_int] (it could be found in the sources
+ simplifies the use of [Big_int] (it can be found in the sources
of Coq). *)
Require Import Arith ZArith.
@@ -105,4 +105,4 @@ Definition check :=
Extraction "/tmp/test.ml" check test.
... and we check that test=check
-*) \ No newline at end of file
+*)
diff --git a/plugins/extraction/ExtrOcamlNatBigInt.v b/plugins/extraction/ExtrOcamlNatBigInt.v
index fb45a8be8..29830d71d 100644
--- a/plugins/extraction/ExtrOcamlNatBigInt.v
+++ b/plugins/extraction/ExtrOcamlNatBigInt.v
@@ -13,7 +13,7 @@ Require Import ExtrOcamlBasic.
(** NB: The extracted code should be linked with [nums.cm(x)a]
from ocaml's stdlib and with the wrapper [big.ml] that
- simlifies the use of [Big_int] (it could be found in the sources
+ simplifies the use of [Big_int] (it can be found in the sources
of Coq). *)
(** Disclaimer: trying to obtain efficient certified programs
diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v
index a6ba9aa2e..6ca5b5fed 100644
--- a/plugins/extraction/ExtrOcamlZBigInt.v
+++ b/plugins/extraction/ExtrOcamlZBigInt.v
@@ -13,7 +13,7 @@ Require Import ExtrOcamlBasic.
(** NB: The extracted code should be linked with [nums.cm(x)a]
from ocaml's stdlib and with the wrapper [big.ml] that
- simlifies the use of [Big_int] (it could be found in the sources
+ simplifies the use of [Big_int] (it can be found in the sources
of Coq). *)
(** Disclaimer: trying to obtain efficient certified programs
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index 07f49cc4f..9010917fe 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -815,7 +815,7 @@ Ltac ring_elements set ext rspec pspec sspec dspec rk :=
fun f => f arth ext_r morph lemma1 lemma2
| _ => fail 4 "ring: bad sign specification"
end
- | _ => fail 3 "ring: bad coefficiant division specification"
+ | _ => fail 3 "ring: bad coefficient division specification"
end
| _ => fail 2 "ring: bad power specification"
end
diff --git a/plugins/setoid_ring/ZArithRing.v b/plugins/setoid_ring/ZArithRing.v
index 3c4f6b86c..cf3a87e1d 100644
--- a/plugins/setoid_ring/ZArithRing.v
+++ b/plugins/setoid_ring/ZArithRing.v
@@ -48,8 +48,8 @@ Ltac Zpower_neg :=
Add Ring Zr : Zth
(decidable Zeq_bool_eq, constants [Zcst], preprocess [Zpower_neg;unfold Z.succ],
power_tac Zpower_theory [Zpow_tac],
- (* The two following option are not needed, it is the default chose when the set of
- coefficiant is usual ring Z *)
+ (* The following two options are not needed; they are the default choice
+ when the set of coefficient is the usual ring Z *)
div (InitialRing.Ztriv_div_th (@Eqsth Z) (@IDphi Z)),
sign get_signZ_th).
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
index 34dc954ec..6896b2d57 100644
--- a/theories/Logic/Hurkens.v
+++ b/theories/Logic/Hurkens.v
@@ -116,7 +116,7 @@ Section Paradox.
(** ** Axiomatisation of impredicative universes in a Martin-Löf style *)
(** System U- has two impredicative universes. In the proof of the
- paradox they are slightly asymetric (in particular the reduction
+ paradox they are slightly asymmetric (in particular the reduction
rules of the small universe are not needed). Therefore, the
axioms are duplicated allowing for a weaker requirement than the
actual system U-. *)