Buenas tardes.
Pude comprobar que para el práctico 7 se entregan múltiples archivos. ¿Hay alguna forma especificada de manejar las dependencias entre módulos? No me estaría funcionando hacer un "Require Import" así sin más como figura en la plantilla de archivo Actions. Parece que hay que definir un archivo _CoqProject pero por ahora no he podido dar con la configuración apropiada para éste.
Otra cuestión, ¿se supone que el archivo Maps lo debemos generar nosotros, sin plantilla? Porque no figura en las plantillas de bibliotecas subidas.
Saludos.