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 /theories/MSets | |
| parent | 5cfdc20560392c2125dbcee31cfd308d5346b428 (diff) | |
Fixing typos - Part 3
Diffstat (limited to 'theories/MSets')
| -rw-r--r-- | theories/MSets/MSetDecide.v | 2 | ||||
| -rw-r--r-- | theories/MSets/MSetGenTree.v | 2 | ||||
| -rw-r--r-- | theories/MSets/MSetInterface.v | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v index f228cbb3bf..3ceff849be 100644 --- a/theories/MSets/MSetDecide.v +++ b/theories/MSets/MSetDecide.v @@ -240,7 +240,7 @@ the above form: True. Proof. intros. push not in *. - (* note that ~(R->P) remains (since R isnt decidable) *) + (* note that ~(R->P) remains (since R isn't decidable) *) tauto. Qed. diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index a3dcca7dfd..838721f499 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -166,7 +166,7 @@ end. *) (** Enumeration of the elements of a tree. This corresponds - to the "samefringe" notion in the litterature. *) + to the "samefringe" notion in the literature. *) #[universes(template)] Inductive enumeration := diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v index 6a18f59fc4..85139593da 100644 --- a/theories/MSets/MSetInterface.v +++ b/theories/MSets/MSetInterface.v @@ -659,7 +659,7 @@ End Raw2Sets. (** It is in fact possible to provide an ordering on sets with very little information on them (more or less only the [In] predicate). This generic build of ordering is in fact not - used for the moment, we rather use a simplier version + used for the moment, we rather use a simpler version dedicated to sets-as-sorted-lists, see [MakeListOrdering]. *) |