Hola Lia.
El manual en línea de Coq está en: https://coq.inria.fr/distrib/current/refman/
La parte de tácticas a las que refiere el práctico 2 aparece en particular en: https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html#tacticals.
El compositor de tácticas que mas van a usar es el ";". Ver: https://coq.inria.fr/refman/proof-engine/ltac.html?highlight=repeat#sequence.
Saludos, Carlos