Exportación básica

Brought to you by: dcalegar, luna3173, slacuesta

#21 Exportación básica

Status: open

Owner: Sebastián Lacuesta

Labels: None

Priority: 9

Updated: 2012-09-29

Created: 2011-07-17

Creator: Sebastián Lacuesta

Private: No

Mediante esta funcionalidad se le brinda la posibilidad al usuario de poder exportar el archivo Coq que se esté manipulando. Una vez seleccionada la opción, se listan los posibles formatos en el que se puede exportar el archivo, estos formatos dependen del motor de Coq ya que se utiliza la herramienta CoqDoc3 para realizar dicha acción. Entre los posibles formatos de salida se encuentran: pdf, ps, html, entre otros.

Discussion

Sebastián Lacuesta - 2011-07-17

Solo pude exportar a LaTex. Técnicamente, latex no es una dependencia de Coop.

If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
- Anonymous
  
  Add attachments
  Cancel
  You seem to have CSS turned off. Please don't fill out this field.
  
  You seem to have CSS turned off. Please don't fill out this field.

Anonymous

Exportación básica

Group

Searches

Help

#21 Exportación básica

Discussion