diff --git a/IntroToProofScripting.v b/IntroToProofScripting.v
index 0097d57..be2367a 100644
--- a/IntroToProofScripting.v
+++ b/IntroToProofScripting.v
@@ -352,7 +352,7 @@ Ltac notHyp P :=
  * levels out from where we are.  [first] applies the first tactic that does not
  * fail. *)
 
-(* This tactic adds a fact to the context, only if it is not not already
+(* This tactic adds a fact to the context, only if it is not already
  * present. *)
 
 Ltac extend pf :=