From 59a8668cb8a3bee4185289f02a0ea22f35915f52 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 5 May 2023 06:45:52 +0000
Subject: [PATCH] Apply 2 suggestion(s) to 1 file(s)

---
 docs/classes.md | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/docs/classes.md b/docs/classes.md
index b4d819ed4..d37d1cbbf 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
-- 
GitLab