From df3a49a18c5b01984000df9244ecea9c275b30cd Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 7 Dec 2015 10:52:14 +0100
Subject: Fix some typos.

---
 plugins/setoid_ring/InitialRing.v    | 6 +++---
 plugins/setoid_ring/Ncring_initial.v | 4 ++--
 2 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'plugins/setoid_ring')

diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index b92b847be5..56023bfb5c 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -155,7 +155,7 @@ Section ZMORPHISM.
    Ltac norm := gen_srewrite Rsth Reqe ARth.
    Ltac add_push := gen_add_push radd Rsth Reqe ARth.
 
-(*morphisms are extensionaly equal*)
+(*morphisms are extensionally equal*)
  Lemma same_genZ : forall x, [x] == gen_phiZ1 x.
  Proof.
   destruct x;simpl; try rewrite (same_gen ARth);rrefl.
@@ -246,7 +246,7 @@ Proof (SRth_ARth Nsth Nth).
 Lemma Neqb_ok : forall x y, N.eqb x y = true -> x = y.
 Proof. exact (fun x y => proj1 (N.eqb_eq x y)). Qed.
 
-(**Same as above : definition of two,extensionaly equal, generic morphisms *)
+(**Same as above : definition of two, extensionally equal, generic morphisms *)
 (**from N to any semi-ring*)
 Section NMORPHISM.
  Variable R : Type.
@@ -671,7 +671,7 @@ End GEN_DIV.
    end.
 
 (* A simple tactic recognizing only 0 and 1. The inv_gen_phiX above
-   are only optimisations that directly returns the reifid constant
+   are only optimisations that directly returns the reified constant
    instead of resorting to the constant propagation of the simplification
    algorithm. *)
 Ltac inv_gen_phi rO rI cO cI t :=
diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v
index c40e0ffbaa..c2eafcdad8 100644
--- a/plugins/setoid_ring/Ncring_initial.v
+++ b/plugins/setoid_ring/Ncring_initial.v
@@ -42,7 +42,7 @@ Defined.
 
 (*Instance ZEquality: @Equality Z:= (@eq Z).*)
 
-(** Two generic morphisms from Z to (abrbitrary) rings, *)
+(** Two generic morphisms from Z to (arbitrary) rings, *)
 (**second one is more convenient for proofs but they are ext. equal*)
 Section ZMORPHISM.
 Context {R:Type}`{Ring R}.
@@ -130,7 +130,7 @@ Ltac rsimpl := simpl.
  Qed.
 
 
-(*morphisms are extensionaly equal*)
+(*morphisms are extensionally equal*)
  Lemma same_genZ : forall x, [x] == gen_phiZ1 x.
  Proof.
   destruct x;rsimpl; try rewrite same_gen; reflexivity.
-- 
cgit v1.2.3