Hola, no me está compilando con esto me da el error:
Error: Cannot find library Maps in loadpath
En cambio Load Maps, me funciona sin problemas. ¿Utilizamos Load?
Saludos,
Jairo.
En respuesta a Jairo Yamil Bonanata Silva
Re: [Práctico 7] Require Export Maps.
Yo en lugar de cambiar la sentencia, lo que hice fué compilar Maps. (Con Maps.v en un buffer, make makefile y luego make), y funcionó.
Hola.
Lo que dice Juan Pablo es correcto.
Usar Load tampoco está mal; pero es preferible la primera opción.
Saludos, Carlos