diff options
| author | Antonio Nikishaev | 2020-04-09 10:48:04 +0400 |
|---|---|---|
| committer | GitHub | 2020-04-09 10:48:04 +0400 |
| commit | 52e091587f9fa65f6184ae5e4c6b63677281376b (patch) | |
| tree | 55572e70281d86f1dd4da10387d4fe9994c5903b /mathcomp/ssreflect | |
| parent | bfd4b28b835e6918d7f4dea848c8b94f4c1c6f7f (diff) | |
Update mathcomp/ssreflect/ssrnat.v
the->this
Co-Authored-By: Yves Bertot <yves.bertot@inria.fr>
Diffstat (limited to 'mathcomp/ssreflect')
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 67bc923..8ddfccb 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -90,7 +90,7 @@ Require Export Ring. (* V (infix) -- disjunction, as in *) (* leq_eqVlt : (m <= n) = (m == n) || (m < n). *) (* X - exponentiation, as in lognX : logn p (m ^ n) = logn p m * n in *) -(* file prime.v (the suffix is not used in the file). *) +(* file prime.v (the suffix is not used in this file). *) (* Suffixes that abbreviate operations (D, B, M and X) are used to abbreviate *) (* second-rank operations in equational lemma names that describe left-hand *) (* sides (e.g., mulnDl); they are not used to abbreviate the main operation *) |