From 74e2399343143e94e8feb56c4bcb00f5cbe15041 Mon Sep 17 00:00:00 2001
From: Samuel Gruetter <samuel.gruetter@epfl.ch>
Date: Sun, 1 Mar 2020 22:30:35 -0500
Subject: [PATCH] explain why recursive [inster] can fail

---
 IntroToProofScripting.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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.