From e48f266b9f2418a619fc1217250fd2942854dcbe Mon Sep 17 00:00:00 2001
From: thery
Date: Mon, 14 Oct 2019 18:06:30 +0200
Subject: typo

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

(limited to 'mathcomp')

diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index d35253c..486b12e 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -94,7 +94,7 @@ From mathcomp Require Import choice fintype finfun bigop prime binomial.
 (*           GRing.rreg x <-> x if right-regular, i.e., *%R x is injective.   *)
 (*               [char R] == the characteristic of R, defined as the set of   *)
 (*                           prime numbers p such that p%:R = 0 in R. The set *)
-(*                           [char p] has a most one element, and is          *)
+(*                           [char R] has at most one element, and is         *)
 (*                           implemented as a pred_nat collective predicate   *)
 (*                           (see prime.v); thus the statement p \in [char R] *)
 (*                           can be read as `R has characteristic p', while   *)
-- 
cgit v1.2.3