diff options
| author | JPR | 2019-05-23 23:28:55 +0200 |
|---|---|---|
| committer | JPR | 2019-05-23 23:28:55 +0200 |
| commit | d306f5428db0d034aea55d3f0699c67c1f296cc1 (patch) | |
| tree | 540bcc09ec46c8a360cda9ed7fafa9ab631d3716 /test-suite/interactive | |
| parent | 5cfdc20560392c2125dbcee31cfd308d5346b428 (diff) | |
Fixing typos - Part 3
Diffstat (limited to 'test-suite/interactive')
| -rw-r--r-- | test-suite/interactive/ParalITP_smallproofs.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/interactive/ParalITP_smallproofs.v b/test-suite/interactive/ParalITP_smallproofs.v index 0d75d52a31..d2e6794c0b 100644 --- a/test-suite/interactive/ParalITP_smallproofs.v +++ b/test-suite/interactive/ParalITP_smallproofs.v @@ -14,7 +14,7 @@ (* 02110-1301 USA *) -(** This file includes random facts about Integers (and natural numbers) which are not found in the standard library. Some of the lemma here are not used in the QArith developement but are rather useful. +(** This file includes random facts about Integers (and natural numbers) which are not found in the standard library. Some of the lemma here are not used in the QArith development but are rather useful. *) Require Export ZArith. @@ -84,7 +84,7 @@ End projection. (*###########################################################################*) -(* Declaring some realtions on natural numbers for stepl and stepr tactics. *) +(* Declaring some relations on natural numbers for stepl and stepr tactics. *) (*###########################################################################*) Lemma le_stepl: forall x y z, le x y -> x=z -> le z y. @@ -173,7 +173,7 @@ Qed. (*###########################################################################*) -(* Declaring some realtions on integers for stepl and stepr tactics. *) +(* Declaring some relations on integers for stepl and stepr tactics. *) (*###########################################################################*) Lemma Zle_stepl: forall x y z, (x<=y)%Z -> x=z -> (z<=y)%Z. |