From 6986032b386babb2eb73e3aa4cdeb0bc5137f8d3 Mon Sep 17 00:00:00 2001
From: gabriel-doriath-dohler <gabriel.doriath.dohler@ens.fr>
Date: Sat, 1 Jan 2022 15:23:08 +0100
Subject: [PATCH] doc: correct the link to "Lean Together 2021: Metaprogramming
 in Lean 4 continued"

---
 doc/syntax.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/syntax.md b/doc/syntax.md
index d1f8d2fc5c..df0ec10986 100644
--- a/doc/syntax.md
+++ b/doc/syntax.md
@@ -24,7 +24,7 @@ both programmers and proof engineers alike.
 
 TODO. See [Lean Together 2021: Metaprogramming in Lean
 4](https://youtu.be/hxQ1vvhYN_U) for an overview as well [the
-continuation](https://youtu.be/hxQ1vvhYN_U) about tactic programming.
+continuation](https://youtu.be/vy4JWIiiXSY) about tactic programming.
 For more information on antiquotations, see also §4.1 of [Beyond
 Notations: Hygienic Macro Expansion for Theorem Proving
 Languages](https://arxiv.org/pdf/2001.10490.pdf#page=11).