From 52e091587f9fa65f6184ae5e4c6b63677281376b Mon Sep 17 00:00:00 2001 From: Antonio Nikishaev Date: Thu, 9 Apr 2020 10:48:04 +0400 Subject: Update mathcomp/ssreflect/ssrnat.v the->this Co-Authored-By: Yves Bertot --- mathcomp/ssreflect/ssrnat.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'mathcomp') 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 *) -- cgit v1.2.3