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/FSets | |
| parent | 5cfdc20560392c2125dbcee31cfd308d5346b428 (diff) | |
Fixing typos - Part 3
Diffstat (limited to 'theories/FSets')
| -rw-r--r-- | theories/FSets/FMapInterface.v | 2 | ||||
| -rw-r--r-- | theories/FSets/FSetDecide.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v index 8970529103..a12e4a43c2 100644 --- a/theories/FSets/FMapInterface.v +++ b/theories/FSets/FMapInterface.v @@ -192,7 +192,7 @@ Module Type WSfun (E : DecidableType). (** Equality of maps *) (** Caveat: there are at least three distinct equality predicates on maps. - - The simpliest (and maybe most natural) way is to consider keys up to + - The simplest (and maybe most natural) way is to consider keys up to their equivalence [E.eq], but elements up to Leibniz equality, in the spirit of [eq_key_elt] above. This leads to predicate [Equal]. - Unfortunately, this [Equal] predicate can't be used to describe diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v index 83bb07ffb6..d977ac05ec 100644 --- a/theories/FSets/FSetDecide.v +++ b/theories/FSets/FSetDecide.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. |