aboutsummaryrefslogtreecommitdiff
path: root/theories/Program
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Program')
-rw-r--r--theories/Program/Tactics.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index e692876dad..6f7645841c 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -101,7 +101,7 @@ Ltac revert_last :=
[ H : _ |- _ ] => revert H
end.
-(** Reapeateadly reverse the last hypothesis, putting everything in the goal. *)
+(** Repeatedly reverse the last hypothesis, putting everything in the goal. *)
Ltac reverse := repeat revert_last.