typo

Co-authored-by: Kim Morrison <[email protected]>
leanprover · Oct 16, 2024 · 7cac8f1 · 7cac8f1
1 parent 9cb310d
commit 7cac8f1
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
@@ -366,7 +366,7 @@ def appendGoals (mvarIds : List MVarId) : TacticM Unit :=
 
 /--
 Discard the first goal and replace it by the given list of goals,
-keeping the other goals. This is used in conjection with `getMainGoal`.
+keeping the other goals. This is used in conjunction with `getMainGoal`.
 
 Contract: between `getMainGoal` and `replaceMainGoal`, nothing manipulates the goal list.