Document enum value changes in provablyDisjointClasses

Author: dwijnand

compiler/src/dotty/tools/dotc/core/TypeComparer.scala

@@ -2772,11 +2772,11 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
    *
    *  1. Single inheritance of classes
    *  2. Final classes cannot be extended
-   *  3. ConstantTypes with distinct values are non intersecting
-   *  4. TermRefs with distinct values are non intersecting
+   *  3. ConstantTypes with distinct values are non-intersecting
+   *  4. TermRefs with distinct values are non-intersecting
    *  5. There is no value of type Nothing
    *
-   *  Note on soundness: the correctness of match types relies on on the
+   *  Note on soundness: the correctness of match types relies on the
    *  property that in all possible contexts, the same match type expression
    *  is either stuck or reduces to the same case.
    */

docs/_spec/03-types.md

@@ -1071,7 +1071,7 @@ The following properties hold about ´⌈X⌉´ (we have paper proofs for those)
 The "lower-bound rule" states that ´S <: T´ if ´T = q.X´ and ´q.X´ is a non-class type designator and ´S <: L´ where ´L´ is the lower bound of the underlying type definition of ´q.X´".
 That rule is known to break transitivy of subtyping in Scala already.
 
-Second, we define the relation ´⋔´ on *classes* (including traits and hidden classes of objects) as:
+Second, we define the relation ´⋔´ on *classes* (including traits, hidden classes of objects, and enum terms) as:
 
 - ´C ⋔ D´ if `´C ∉´ baseClasses´(D)´` and ´D´ is `final`
 - ´C ⋔ D´ if `´D ∉´ baseClasses´(C)´` and ´C´ is `final`