diff options
Diffstat (limited to 'theories/FSets')
| -rw-r--r-- | theories/FSets/FSetAVL.v | 2 | ||||
| -rw-r--r-- | theories/FSets/FSetEqProperties.v | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v index 3c9b6b428b..dcaea894eb 100644 --- a/theories/FSets/FSetAVL.v +++ b/theories/FSets/FSetAVL.v @@ -15,7 +15,7 @@ It follows the implementation from Ocaml's standard library, All operations given here expect and produce well-balanced trees - (in the ocaml sense: heigths of subtrees shouldn't differ by more + (in the ocaml sense: heights of subtrees shouldn't differ by more than 2), and hence has low complexities (e.g. add is logarithmic in the size of the set). But proving these balancing preservations is in fact not necessary for ensuring correct operational behavior diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v index 56844f4773..59b2f789ab 100644 --- a/theories/FSets/FSetEqProperties.v +++ b/theories/FSets/FSetEqProperties.v @@ -333,7 +333,7 @@ Proof. auto with set. Qed. -(* caracterisation of [union] via [subset] *) +(* characterisation of [union] via [subset] *) Lemma union_subset_1: subset s (union s s')=true. Proof. @@ -408,7 +408,7 @@ intros; apply equal_1; apply inter_add_2. rewrite not_mem_iff; auto. Qed. -(* caracterisation of [union] via [subset] *) +(* characterisation of [union] via [subset] *) Lemma inter_subset_1: subset (inter s s') s=true. Proof. |