diff --git a/IntroToProofScripting.v b/IntroToProofScripting.v
index af0aa45..8f514e5 100644
--- a/IntroToProofScripting.v
+++ b/IntroToProofScripting.v
@@ -518,7 +518,8 @@ Ltac inster n :=
         end
     end.
 
-(* Important: when one recursive call fails, the backtracking semantics of
+(* Important: when one recursive call fails (happens when [n] reaches zero and
+ * [intuition] leaves some open goals), the backtracking semantics of
  * [match goal] cause us to try the next instantiation! *)
 
 Section test_inster.