From 2d032b5330adc7e7d7dcf0fb0daf593bffe280ec Mon Sep 17 00:00:00 2001
From: Assia Mahboubi
Date: Mon, 30 Nov 2015 15:52:24 +0100
Subject: Typos in comments.

---
 mathcomp/field/fieldext.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/field')

diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v
index eb1b6be..1e14ab7 100644
--- a/mathcomp/field/fieldext.v
+++ b/mathcomp/field/fieldext.v
@@ -67,7 +67,7 @@ Require Import poly polydiv mxpoly generic_quotient.
 (*                           in turn has an extFieldType F0 structure.        *)
 (*           baseVspace V == the subspace of baseFieldType L that coincides   *)
 (*                           with V : {vspace L}.                             *)
-(* --> Some caution muse be exercised when using fieldOver and basFieldType,  *)
+(* --> Some caution must be exercised when using fieldOver and baseFieldType, *)
 (*     because these are convertible to L while carrying different Lmodule    *)
 (*     structures. This means that the safeguards engineered in the ssralg    *)
 (*     library that normally curb the Coq kernel's inclination to diverge are *)
-- 
cgit v1.2.3