From 65c8d91cd4c11b8de44f0b23cd44a3303cd54d4e Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 27 Oct 2014 07:21:09 +0100
Subject: Fix some typos in comments.

---
 plugins/extraction/ExtrOcamlBigIntConv.v | 4 ++--
 plugins/extraction/ExtrOcamlNatBigInt.v  | 2 +-
 plugins/extraction/ExtrOcamlZBigInt.v    | 2 +-
 plugins/setoid_ring/InitialRing.v        | 2 +-
 plugins/setoid_ring/ZArithRing.v         | 4 ++--
 5 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/ExtrOcamlBigIntConv.v b/plugins/extraction/ExtrOcamlBigIntConv.v
index 265fbc52cb..3a9e7cd8ee 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 fb45a8be83..29830d71db 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 a6ba9aa2e9..6ca5b5fedc 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 07f49cc4ff..9010917fec 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 3c4f6b86cf..cf3a87e1d8 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).
 
-- 
cgit v1.2.3