My goal with this tutorial was to introduce the core aspects of the language (dependent types, tactics, etc.) from first principles. If you're fascinated by proof assistants like Coq or Lean and want to understand how to use them, this tutorial is written for you.
I've done Logical Foundations and part of Programming Language Foundations, and some of the stuff in your tutorial is new to me (especially dependent types).
Your tutorial is very interesting, but in comparison to the Software Foundations series you have relatively few exercises and they're all at the end of the chapter. I found it helpful to do exercises as I went along, in many cases testing or exercising my knowledge of a new concept or Coq feature right away. So I would suggest writing more exercises and sprinkling them closer to where some of the material is introduced.
Also, some of your exercises in some chapters have a pretty steep ramp-up in difficulty, so again it might be nice to have exercises that gradually build in difficulty.
These are probably important considerations when readers are going to be working through this material entirely on their own and it might be their first exposure to Coq. (I think your tutorial says it was previously presented in-person, which has got to be a lot easier, since people can ask questions!)
My goal with this tutorial was to introduce the core aspects of the language (dependent types, tactics, etc.) from first principles. If you're fascinated by proof assistants like Coq or Lean and want to understand how to use them, this tutorial is written for you.
Any feedback is appreciated!