From 2ef93d36fc66b9f5010dab4f1c0c6702892c5114 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 19 Feb 2023 13:42:53 -0500 Subject: [PATCH] Typo fix --- IntroToProofScripting.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 :=