From d9fb7fca94af70c11e683ef2818d25cd850999eb Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sun, 23 Apr 2023 16:09:47 -0400
Subject: [PATCH] Wrong tactic name in comment

---
 DependentInductiveTypes.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/DependentInductiveTypes.v b/DependentInductiveTypes.v
index 80816c7..2afd5ca 100644
--- a/DependentInductiveTypes.v
+++ b/DependentInductiveTypes.v
@@ -457,7 +457,7 @@ Proof.
   (* A nasty error message greets us!  The book's [cases] tactic could be
    * extended to handle this case, but we don't generally need to do case
    * analysis on dependently typed values, outside the one excursion of this
-   * "bonus" source file.  Still, the book defines a tactic [dep_case] that
+   * "bonus" source file.  Still, the book defines a tactic [dep_cases] that
    * mostly appeals to built-in tactic [dependent destruction]. *)
 
   dep_cases (cfold e1).