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.