Funciona parcialmente, ocasionalmente se inserta una línea al comienzo del archivo y no hay manera de corregir eso, también se tranca el intérprete debido a eso.
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
En caso de que no se esté manipulando ningún archivo Coq, esta funcionalidad permanecerá deshabilitada. Las instrucciones ejecutadas deberán cambiar de color.
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
Funciona parcialmente, ocasionalmente se inserta una línea al comienzo del archivo y no hay manera de corregir eso, también se tranca el intérprete debido a eso.
Esta funcionalidad está disponible en la barra de herramientas de la perspectiva asociada al IDE Coq.
En caso de que no se esté manipulando ningún archivo Coq, esta funcionalidad permanecerá deshabilitada. Las instrucciones ejecutadas deberán cambiar de color.