diff --git a/docs/classes.md b/docs/classes.md
index b4d819ed4874914165c69bbe6065d4505ebaf2d0..d37d1cbbf3a0a15a1701c157f30b3220eccb5e7f 100644
--- a/docs/classes.md
+++ b/docs/classes.md
@@ -72,14 +72,15 @@ Global Hint Cut [_* persistent_separable and_persistent] : typeclass_instances.
 
 This hint says that at any point during the instance search (`_*`), if
 `persistent_separable` has been applied, the next instance to be applied should
-**not** be `and_persistent`.
+**not** be `and_persistent`. This rules out the derivation on the right
+in the example above.
 
 **Warning from the Coq reference manual:** The regexp matches the entire path.
 Most hints will start with a leading `_*` to match the tail of the path.
 
 The order matters. Having a cut for `[_* and_persistent persistent_separable]`
 (i.e., excluding the first derivation) would result in incompleteness. It
-become impossible to derive `Separable (P ∧ Q)` from `Persistent P` and
+becomes impossible to derive `Separable (P ∧ Q)` from `Persistent P` and
 `Separable Q`.
 
 Note that `Separable` is not closed under `∀`, but `Persistent` is. Hence we