Hola.
Esta táctica no se usa (no se precisa usar en el práctico); no se si la comentaron en el teórico.
Hay información (y un ejemplo) en:
https://coq.inria.fr/distrib/current/refman/Reference-Manual011.html#@default513.
Puede usarse para dar un término de prueba (típicamente una función) incompleto (usando _); que luego será refinado. Con un exact uno tiene que dar exactamente el término de prueba.
Saludos, Carlos