Coq: ¿definiciones de Ltac sobre listas de argumentos variables?

Al intentar crear una definición Ltac que recorre una lista de argumentos de longitud variable, me encontré con el siguiente comportamiento inesperado en Coq 8.4pl2. ¿Puede alguien explicármelo? Ltac ltac_loop X := match X with | 0 => idtac ...