diff options
Diffstat (limited to 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Cyclic31.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZPow.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NStrongRec.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Rational/BigQ/BigQ.v | 2 |
4 files changed, 4 insertions, 4 deletions
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index 1be361b66..98f84a60c 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -654,7 +654,7 @@ Section Basics. f_equal; auto. Qed. - (** This equivalence allows to prove easily the following delicate + (** This equivalence allows proving easily the following delicate result *) Lemma EqShiftL_twice_plus_one : forall k x y, diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v index 26d5ffef0..e8fd2c6b3 100644 --- a/theories/Numbers/NatInt/NZPow.v +++ b/theories/Numbers/NatInt/NZPow.v @@ -30,7 +30,7 @@ Module Type NZPowSpec (Import A : NZOrdAxiomsSig')(Import B : Pow' A). End NZPowSpec. (** The above [pow_neg_r] specification is useless (and trivially - provable) for N. Having it here allows to already derive + provable) for N. Having it here already allows deriving some slightly more general statements. *) Module Type NZPow (A : NZOrdAxiomsSig) := Pow A <+ NZPowSpec A. diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v index f98e8da9a..afd685ba9 100644 --- a/theories/Numbers/Natural/Abstract/NStrongRec.v +++ b/theories/Numbers/Natural/Abstract/NStrongRec.v @@ -24,7 +24,7 @@ Variable A : Type. Variable Aeq : relation A. Variable Aeq_equiv : Equivalence Aeq. -(** [strong_rec] allows to define a recursive function [phi] given by +(** [strong_rec] allows defining a recursive function [phi] given by an equation [phi(n) = F(phi)(n)] where recursive calls to [phi] in [F] are made on strictly lower numbers than [n]. diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v index 50c90757a..e866a52d6 100644 --- a/theories/Numbers/Rational/BigQ/BigQ.v +++ b/theories/Numbers/Rational/BigQ/BigQ.v @@ -33,7 +33,7 @@ Module BigN_BigZ <: NType_ZType BigN.BigN BigZ. Qed. End BigN_BigZ. -(** This allows to build [BigQ] out of [BigN] and [BigQ] via [QMake] *) +(** This allows building [BigQ] out of [BigN] and [BigQ] via [QMake] *) Delimit Scope bigQ_scope with bigQ. |