From 845ac365c952ed8eb61e21ab0ce61c59545639cb Mon Sep 17 00:00:00 2001
From: fengfeng-zi <269969865+fengfeng-zi@users.noreply.github.com>
Date: Thu, 7 May 2026 14:18:28 +0800
Subject: [PATCH] docs: update Ltac2 source links to rocq-prover

---
 src/ltac2_tutorial.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/ltac2_tutorial.v b/src/ltac2_tutorial.v
index 6acbe20..7e0feaf 100644
--- a/src/ltac2_tutorial.v
+++ b/src/ltac2_tutorial.v
@@ -55,11 +55,11 @@ Ltac2 Eval Message.print (Message.of_constr '(3+4)).
 (*+ Reading the Ltac2 source *)
 
 (* You will need to read the Ltac2 source
-(https://github.com/coq/coq/tree/master/user-contrib/Ltac2) to figure out how
+(https://github.com/rocq-prover/rocq/tree/master/plugins/ltac2) to figure out how
 things work. This ranges from fine to totally impossible.
 
 For example, let's figure out the Message API. We open
-https://github.com/coq/coq/blob/master/user-contrib/Ltac2/Message.v and look at
+https://github.com/rocq-prover/rocq/blob/master/plugins/ltac2/Message.v and look at
 what's there. It doesn't have a type [Message.t] but just [message], so find
 it's definition - it's defined as [Ltac2 Type message], which means it comes
 from OCaml. That's fine, it's opaque anyway.