From b3af7fbe888c0b405022d7bd35a647823cd682e3 Mon Sep 17 00:00:00 2001
From: Laurent Théry
Date: Thu, 14 Nov 2019 10:36:25 +0100
Subject: typo (#412)

---
 mathcomp/field/finfield.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp')

diff --git a/mathcomp/field/finfield.v b/mathcomp/field/finfield.v
index cb499b3..b184ed7 100644
--- a/mathcomp/field/finfield.v
+++ b/mathcomp/field/finfield.v
@@ -453,10 +453,10 @@ Qed.
 End FinSplittingField.
 
 Section FinFieldExists.
-(* While he existence of finite splitting fields and of finite fields of      *)
+(* While the existence of finite splitting fields and of finite fields of     *)
 (* arbitrary prime power order is mathematically straightforward, it is       *)
 (* technically challenging to formalize in Coq. The Coq typechecker performs  *)
-(* poorly for the spme of the deeply nested dependent types used in the       *)
+(* poorly for some of the deeply nested dependent types used in the           *)
 (* construction, such as polynomials over extensions of extensions of finite  *)
 (* fields. Any conversion in a nested structure parameter incurs a huge       *)
 (* overhead as it is shared across term comparison by call-by-need evalution. *)
-- 
cgit v1.2.3