aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNick Lewycky2018-08-17 19:58:26 -0700
committerNick Lewycky2018-08-17 19:58:26 -0700
commit1f1585b1181a83c6d386ed63b6f40784d6e69fe9 (patch)
treef96500d0a49a46adfca7dad4df22cbec148af43b
parent8155ba54ae39dd71c6b8ddff2b2b7353dde9aff8 (diff)
Fix typo in documentation, heigth --> height.
-rw-r--r--theories/FSets/FSetAVL.v2
-rw-r--r--theories/MSets/MSetGenTree.v2
2 files changed, 2 insertions, 2 deletions
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index df627a14bd..4d51da4436 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -13,7 +13,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/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v
index 036ff1aa4b..caf5ec4bac 100644
--- a/theories/MSets/MSetGenTree.v
+++ b/theories/MSets/MSetGenTree.v
@@ -11,7 +11,7 @@
This module factorizes common parts in implementations
of finite sets as AVL trees and as Red-Black trees. The nodes
of the trees defined here include an generic information
- parameter, that will be the heigth in AVL trees and the color
+ parameter, that will be the height in AVL trees and the color
in Red-Black trees. Without more details here about these
information parameters, trees here are not known to be
well-balanced, but simply binary-search-trees.