From d306f5428db0d034aea55d3f0699c67c1f296cc1 Mon Sep 17 00:00:00 2001
From: JPR
Date: Thu, 23 May 2019 23:28:55 +0200
Subject: Fixing typos - Part 3

---
 theories/Numbers/NatInt/NZAddOrder.v | 2 +-
 theories/Numbers/NatInt/NZDomain.v   | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'theories/Numbers/NatInt')

diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v
index 5f102e853b..b96a2b35af 100644
--- a/theories/Numbers/NatInt/NZAddOrder.v
+++ b/theories/Numbers/NatInt/NZAddOrder.v
@@ -149,7 +149,7 @@ Proof.
 intros n m H; apply add_le_cases; now nzsimpl.
 Qed.
 
-(** Substraction *)
+(** Subtraction *)
 
 (** We can prove the existence of a subtraction of any number by
     a smaller one *)
diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v
index acebfcf1d2..cace65c61d 100644
--- a/theories/Numbers/NatInt/NZDomain.v
+++ b/theories/Numbers/NatInt/NZDomain.v
@@ -310,7 +310,7 @@ Qed.
 End NZOfNatOrd.
 
 
-(** For basic operations, we can prove correspondance with
+(** For basic operations, we can prove correspondence with
     their counterpart in [nat]. *)
 
 Module NZOfNatOps (Import NZ:NZAxiomsSig').
-- 
cgit v1.2.3