Hola!
La generación de nombres automáticos por parte de Coq ha venido variando en diferentes versiones.
Para desarrollos medianos y grandes, en particular, es altamente recomendable asignar nombres y usar tácticas propias (definidas) para que los desarrollos sean relativamente independientes de nuevas versiones del software. Al igual que en los lenguajes de programación, es útil que los nombres de variables sean representativos, para dar claridad a las pruebas.
Saludos, Carlos