Hola,
Al momento de llegar a la linea "End P1." en el template del practico 1, me sale el siguiente error y no me deja continuar:
Error: Proof editing in progress.
Proofs currently edited: e63 e62 e61 e55 e54 e53 e52 e51 e48 e47 e46 e45 e44
e43 e42 e41 e32 e31 e22 e21 e13 e12
e11.
Use "Abort All" first or complete proof(s).
Aclaro que no tengo ninguna prueba incompleta, pero supongo que algo me falta hacer.
Estoy trabajando con el CoqIDE para windows y Coq 8.4p16
Gracias!